The Coq mailing list

[Frederic Loulergue <frederic.loulergue AT univ-orleans.fr>]

    Dear all,

Two postdoctoral researcher positions are available at the University of Orléans, France.
    The successful candidates will be members of the LMV team of the Computer Science Laboratory of Orléans (LIFO), Orléans site. The city is in the heart of the Loire Valley, an outstanding cultural landscape classified as a UNESCO World Heritage Site in 2000.
    CoMeMoV Project

A Post-Doctoral position is available as part of the CoMeMoV project between LIFO (University of Orleans, France), CEA List and Thales Research and Technology.

Frama-C is an extensible and collaborative open-source platform dedicated to source-code analysis of C software. If offers a specification language and various analyzers in the form of separate plugins. The WP plugin of Frama-C can be used to prove that a given C program respects its specification. WP provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial-strength programs, this combination already makes WP mature enough to be deployed for proving critical industrial embedded software. However, several theoretical and practical issues still persist. The goal of CoMeMoV is to tackle these issues to allow deductive verification with WP to better scale on complex industrial programs.

The work of the successful candidate will mainly focus on the formalization and proof of correctness of the proposed collaborative memory models for deductive verification (WP3).

Application requirements:

- PhD (obtained or to be obtained soon) in Computer Science
- Technical background in formal methods, in particular, in interactive theorem proving
- Technical background in programming in C
- Communication skills and teamwork capabilities
- English language fluency in both speaking and writing

The position is available immediately. This is a research-only position, for 21 months. 

Please send the application materials (CV and cover letter) or any questions to Frederic Loulerge.

The deadline for application is December 23, 2023.

AcceptAlgo Project

A Post-Doctoral position is available as part of the AcceptAlgo, a two-year project funded by Région Centre Val de Loire. The partners are two institutes of the University of Orleans: the Orleans Economics Laboratory (LEO) and the Computer Science Laboratory of Orleans (LIFO).

Individuals have seen their exposure to algorithms increase considerably over the past decade. This exposure is exercised mainly in direct interaction with computers, telephones or other connected objects, during many moments of the social and economic life of individuals, but also in administrative or technical procedures of professionals. Individuals interact with algorithms when searching for information on the internet, when using connected medical devices, when delegating the management of their savings and retirement or when making online purchases. This research project aims to study how individuals evaluate and accept algorithms presented in mathematical form and in simple language form i.e. with words intelligible by individuals. It consists in measuring the acceptability for individuals of the algorithms presented through these simplified explanations.

The role of the postdoctoral researcher in this project is to improve and extend SyDPaCC, a framework for the Coq proof assistant to develop correct functional scalable parallel programs from sequential specifications.

Application requirements: 

- PhD (obtained or to be obtained soon) in Computer Science
- Technical background in formal methods, in particular, in interactive theorem proving
- Technical background in scalable parallel programming
- Communication skills and teamwork capabilities
- English language fluency in both speaking and writing 

The position is available immediately but may start from Summer 2024. This is a research-only position, for 12 months.

Please send the application materials (CV and cover letter) or any questions to Frederic Loulerge. 

The deadline for application is January 31, 2024.

Best regards,

Frederic Loulergue

--

Professeur
Université d'Orléans
UFR Collegium Sciences & Techniques
Laboratoire d'Informatique Fondamentale d'Orléans (LIFO)
Responsable de l'équipe LMV - Langages Modèles et Vérification
https://frederic.loulergue.eu