Sciweavers

ENTCS
2006

A Verified Compiler for Synchronous Programs with Local Declarations

13 years 3 months ago
A Verified Compiler for Synchronous Programs with Local Declarations
In addition to efficient code generation, causality cycles and schizophrenic statements are major problems for the compilation of synchronous programs. Although these problems are already solved by existing compilers, there is still a need for clean and efficient compilation techniques. In this paper, we describe a complete and efficient compilation of programs from the Esterel family to equivalent equation systems. Our translation is even able to solve schizophrenia problems for data flows with delayed statements. The overall compilation runs in time quadratic to the length of the program and has been formally verified with the HOL theorem prover.
Klaus Schneider, Jens Brandt, Tobias Schüle
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Klaus Schneider, Jens Brandt, Tobias Schüle
Comments (0)