Skip to Main content Skip to Navigation
Conference papers

Formal verification of automatically generated C-code from polychronous data-flow equations

van Chan Ngo 1 Loic Besnard 1 Thierry Gautier 1 Paul Le Guernic 1 Jean-Pierre Talpin 1 
1 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Synchronous data-flow languages are used as design approaches in developing embedded and critical real-time systems in which synchronous programs are verified by applying formal verification. In a synchronous design approach, transformation and optimization are used to transform synchronous programs and generate general purpose executable code. The incorrectness of the transformations make the guarantees unable to carry over the transformed programs and the executable code. In this work, adopting the translation validation approach, we present an automated verification process to verify the correctness of the synchronous language compiler Signal transformations and code generation on the clock information.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Van Chan Ngo Connect in order to contact the contributor
Submitted on : Wednesday, December 12, 2012 - 11:07:54 AM
Last modification on : Friday, February 4, 2022 - 3:12:45 AM
Long-term archiving on: : Sunday, December 18, 2016 - 12:08:58 AM


Files produced by the author(s)


  • HAL Id : hal-00763781, version 1


van Chan Ngo, Loic Besnard, Thierry Gautier, Paul Le Guernic, Jean-Pierre Talpin. Formal verification of automatically generated C-code from polychronous data-flow equations. HLDVT 2012 - IEEE International High-Level Design, Validation and Test Workshop, Nov 2012, California, United States. ⟨hal-00763781⟩



Record views


Files downloads