Frama-C/Synchrone

Sep 1, 2026
Go to Project Site

Frama-C/Synchrone extracts synchronous Lustre models from reactive C programs. The extracted models can be augmented with synchronous observers and verified using model checkers such as Kind2 and GATeL.

Fabien Siron
Fabien Siron
Research Engineer | Lecturer

Research engineer working on formal verification, synchronous-reactive systems and safety-critical real-time software.

Publications

Modular Extraction of Lustre Models from C Reactive Programs using Frama-C
Extraction of synchronous Lustre models from reactive C programs by combining symbolic program analysis and abstract interpretation in Frama-C.
Loïc Correnson, Fabien Siron, Christophe Junke
Project Source Document DOI