CoMeMoV

Collaborative Memory Models for formal Verification

Home | News | Jobs | Publications | Work Packages | Deliverables |

Jobs

Post-doctoral Researcher

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:

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

The successful candidate will be a member of the LMV team of the Computer Science Laboratory of Orléans (LIFO) on its Orléans site. The city in in the heart of the Loire Valley, an outstanding cultural landscape classified as a UNESCO World Heritage Site in 2000.

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

The deadline for application is December 23, 2023.

Internships

The CoMeMoV partners often have opportunities for internships at the undergraduate level (LIFO, University of Orleans) and at the graduate level (all partners). If you are interested in an internship send a CV and a cover letter indicating in particular which part of the project your are interested in and which partner you would like to join.