Modular Extraction of Lustre Models from C Reactive Programs using Frama-C

Loïc Correnson, Fabien Siron, Christophe Junke
September, 2026
Project Source Document DOI

Abstract

This work presents Frama-C/Synchrone, a methodology and plug-in for extracting synchronous-reactive models from cyclic C programs. The approach constructs a symbolic transition system using program-analysis techniques and simplifies memory interactions in order to generate Lustre models that can subsequently be analyzed by synchronous verification tools.

Type
Journal article
Publication
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD) — EMSOFT 2026
Formal Verification Frama-C Lustre Synchronous-Reactive Systems Program Analysis
Fabien Siron
Fabien Siron
Research Engineer | Lecturer

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