Formal Verification

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
Methodology for the Formal Verification of Temporal Properties for Real-Time Safety-Critical Applications Based on Logical Time
PhD thesis on semantic foundations and formal verification of logical-time real-time programs, with applications to PsyC, synchronous languages, symbolic model checking, and CCSL.
Fabien Siron
PDF Slides Source Document
Semantics Foundations of PsyC Based on Synchronous Logical Execution Time
Semantic foundations for the industrial PsyC language based on Synchronous Logical Execution Time, relating LET-style execution to synchronous-reactive semantics.
Fabien Siron, Dumitru Potop-Butucaru, Robert de Simone, Damien Chabrol, Amira Methni
PDF Source Document DOI
Vérification d'applications temps-réel basées sur le paradigme de Logical Execution Time (LET)
French doctoral-session paper on adapting verification techniques from synchronous languages to real-time applications based on Logical Execution Time.
Fabien Siron, Dumitru Potop-Butucaru, Robert de Simone, Damien Chabrol, Amira Methni
PDF Source Document
Programming and Verifying Real-Time Design Using Logical Time
Early work comparing synchronous languages, Logical Execution Time, and PsyC with the objective of reusing synchronous verification techniques for LET-based real-time programs.
Fabien Siron, Dumitru Potop-Butucaru, Robert de Simone, Damien Chabrol, Amira Methni
PDF Source Document