CoMeMoV: Collaborative Memory Models for formal Verification


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.