Representation predicates for deductive verification

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.

Application of formal methods for interferences management

Within a multidisciplinary technological research team of experts in SW/HW co-design tools by applying formal methods, you will be involved in a national research project aiming at developing an environment to identify, analyze and reduce the interferences generated by the concurrent execution of applications on a heterogeneous commercial-off-the-shelf (COTS) multi-core hardware platform.

Top