While Frama-C was successfully used for deductive verification in various case studies, recent industrial applications conducted at Thales Research and Technology demonstrated the need for significant enhancements of the tool to make it possible to efficiently and soundly realise deductive verification of real-life industrial software products with >10k lines of code mixing complex data-structures, dynamic memory allocation and low-level constructs such as bitfields, unions and memory casts. The Frama-C/WP plugin 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 industrial critical embedded software. However, several theoretical and practical issues still persist. The goal of CoMeMoV is to tackle these issues to scale on deductive verification of complex programs.
CoMeMoV is funded by ANR (ANR-22-CE25-0018).
Partners
- CEA LIST
- Université d’Orléans (lead partner)
- Thales Research & Technology
Members
- Téo Bernier, Thales Research & Technology
- Allan Blanchard, CEA LIST
- Myriam Clouet, Université d’Orléans
- Loïc Correnson, CEA LIST
- Jéméry Damour, CEA LIST & Université d’Orléans
- Nikolai Kosmatov, Thales Research & Technology
- Delphine Longuet, Thales Research & Technology
- Frédéric Loulergue, PI, Université d’Orléans
- Yani Ziani, Thales Research & Technology & Université d’Orléans