A Verified Compiler for Synchronous Programs with Local Declarations

In: Electronic Notes in Theoretical Computer Science (ENTCS). Volume 153, Number 4, Elsevier, P. 71-97, 2006

Authors

• Klaus Schneider
• Jens Brandt
• Tobias Schüle

Abstract

We describe the translation of Esterel-like programs with delayed actions to equivalent transition relations and equation systems. Potential schizophrenia problems arising from local declarations are solved by (1) generating copies of the surface of the statement and (2) renaming the local variables in these copies to allow them to have different values at the same point of time. The translation runs in polynomial time and has been formally verified with the HOL theorem prover.

Full Text

• Publication: ScBS06.pdf

BibTeX

 
@Article{ ScBS06, 
   title = { A Verified Compiler for Synchronous Programs with Local Declarations }, 
   author = { Klaus Schneider and Jens Brandt and Tobias Schüle },    
   journal = { Electronic Notes in Theoretical Computer Science (ENTCS) },  
   volume = { 153 }, 
   number = { 4 },    
   publisher = { Elsevier },   
   pages = { 71-97 },   
   year = 2006, 
} 

---

This publication belongs to the project EVAS.