Postdoctoral Researcher in formal methods applied to configuration management languages

UNIVERSITE D'ORLEANS; France; Sur place; EUR 24 000 - 30 000; Plein temps

Résumé du poste

A university in France is seeking a PhD candidate for a position in the field of computer science. The successful candidate will focus on mechanized formal semantics and program transformations using tools such as Rocq. Key qualifications include a PhD in computer science, proficiency in English, and experience with formal methods. The role involves collaboration within the For-CoaLa team, working on cybersecurity and reliability in software applications.

Qualifications

• PhD in computer science is required.
• Experience in formal methods must be evidenced by publications.
• Ability to communicate effectively in English, both verbally and in writing.

Responsabilités

• Contribute to design and development of mechanized formal semantics.
• Ensure correctness of program transformations using relevant tools.
• Disseminate knowledge from the For-CoaLa project.

Connaissances

Ability to work in a team

Written and oral communication skills in English

Experience in formal methods

Proficiency in collaborative tools (Git, LaTeX)

Familiarity with Infrastructure-as-Code tools

Formation

PhD in computer science

Outils

Git

LaTeX

Rocq proof assistant

Description du poste

Offer Description

Organisation/Company UNIVERSITE D'ORLEANS Research Field Computer science Researcher Profile Recognised Researcher (R2) Positions PhD Positions Country France Application Deadline 26 Jan 2026 - 12:00 (Europe/Paris) Type of Contract Temporary Job Status Full-time Hours Per Week 37h30 Is the job funded through the EU Research Framework Programme? Not funded by a EU programme Is the Job related to staff position within a Research Infrastructure? No

Presentation of the project

Large distributed software systems (applications or infrastructures) are now ubiquitous, with component-based systems (e.g., service-oriented architectures or microservices) offering a convenient way to structure large systems, in particular distributed systems deployed in the Cloud, in the core, or at the edge of the network. DevOps operations, that include system configurations and reconfigurations, are required to handle various kinds of scenarios such as fault tolerance, scalability, software updates, or various optimizations, etc. Such changes may lead to faults. A study of 597 unplanned outages that affected popular cloud services between 2009 and 2015 found that 16% of them were caused by a system upgrade.

Presentation of the service / laboratory

Since 2015, the overall objective of the Languages, Modeling, Verification (LMV) team is to advance the reliability and security of software, particularly in the context of the Internet of Things (IoT). This objective is part of the general field of cybersecurity. We aim to ensure that the software involved satisfies critical properties either by construction by leveraging the design of libraries and programming languages, or by using formal methods. We consider both so-called transformational programs—which terminate and produce a single result from input data—and reactive programs—which do not terminate and interact continuously with their environment and whose behaviors are characterized by temporal descriptions. The programs we consider are embedded software whether they are applications, operating system components, security‑critical modules, software dealing with the deployment, configuration and reconfiguration of distributed applications on the Internet of Things, as well as parallel programs for the analysis of massive data from the IoT. We rely on several branches of formal methods including, among others, the theoretical foundations of the semantics of programming languages, typing, deductive verification but also rewriting systems, static analysis and the combination of techniques. In most of our work, we use the Rocq proof assistant to generate certified code when relevant or, at least, to strengthen confidence in the results obtained, or to complement the use of other formal methods.

Presentation of the missions

The successful candidate will contribute to the design and development of mechanized formal semantics, proofs of their properties as well as program transformations and proofs of their correctness, primarily using the Rocq proof assistant, but also potentially the Why3 proof environment or the Maude system. They will contribute to disseminating knowledge from the For‑CoaLa project in various ways.
The successful candidate will be part of the For‑CoaLa team, which currently consists of a professor and two associate professors, a doctoral student, and a part-time research engineer at the University of Orléans and IMT Atlantique (Nantes).

Presentation of the profile

• PhD in computer science
• Ability to work in a team
• Written and oral communication skills in English
• Experience in formal methods is required, as evidenced by publications and software development
• Proficiency in collaborative tools, including Git and LaTeX
• Familiarity with one or more Infrastructure-as-Code tools is preferred

Additional Information

Work Location(s)

Number of offers available 1 Company/Institute LIFO laboratory Country France City Orléans Postal Code 45100 Street Campus universitaire d'Orléans la Source