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.
The WP tool of Frama-C does not use separation logic. An ongoing research project aims at integrating elements from separation logic into WP, in order to improve performances and the ability to deal with complex data-structures. However, the proposed extension does not allow verifying programs with recursive data-structures, for this, we need the representation precidates from separation logic. The goal of this postdoc is to study how to integrate them in WP.