Frama-C is a collaborative platform for analysis of C programs. Among the different tools available in Frama-C, WP is dedicated to deductive verification of programs, allowing mathematical proof of functional properties and absence of runtime errors. This tool is used for years in industry.
Separation logic is the most promising way to allow verification of properties for programs involving complex data structures. However, it is hard to use for industrial use-cases. The main reason for this is that it is hard to encode into automatic proof tools. Thus, its use requires a lot of work from users.
In a recent work, we described how to extend WP tooling tout describe the memory footprint of C data-structures. The idea is to provide a specification language that allows to capture most of the power of separation logic without having to encode it in proof tools. The goal of this postdoc is to experiment the use of this formalism to describe real world use cases and implement its support in Frama-C and WP.