About us
Espace utilisateur
INSTN offers more than 40 diplomas from operator level to post-graduate degree level. 30% of our students are international students.
Professionnal development
Professionnal development
Find a training course
INSTN delivers off-the-self or tailor-made training courses to support the operational excellence of your talents.
Human capital solutions
At INSTN, we are committed to providing our partners with the best human capital solutions to develop and deliver safe & sustainable projects.
Home   /   Post Doctorat   /   Representation predicates for deductive verification

Representation predicates for deductive verification

Computer science and software Cyber security : hardware and sofware Engineering sciences Technological challenges


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.


Département Ingénierie Logiciels et Systèmes (LIST)
Laboratoire pour la Sûreté du Logiciel
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down