The Synchrone plug-in of Frama-C is dedicated to Lustre programs analysis. It combines the capabilities of the WP and Eva plug-ins and interacts with the GaTeL solver to prove different properties about analyzed programs. This postdoc aims at improving the whole usage of Synchrone throught the following scientific challenges:
- develop a verification methodology that relies on the combination of technics available in the tool, by applying it to representative use-cases,
- in order to support this methodoogy, improve the tools available in Synchrone, in particular the generation of the proof obligations, and their optimization for automatic solvers, like the Colibri2 solver which is developed in the lab,
- improve the link between what the tool verifies and the mathematical specification of the system, by extending LustreSpec and developping associated tools, it comprises aspects related to numerical filters,
- development of tools for visualizing and debugging proof obligations.

This postdoc thus aims at having a global view of the Synchrone tool, targeting publications about proof methodology in an industrial context.