Formal verification of a synchronous data-flow compiler : from Signal to C
Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code...
Main Author: | |
---|---|
Language: | English |
Published: |
Université Rennes 1
2014
|
Subjects: | |
Online Access: | http://tel.archives-ouvertes.fr/tel-01067477 http://tel.archives-ouvertes.fr/docs/01/06/74/77/PDF/NGO_Van_Chan.pdf |