Embedding imperative synchronous languages in interactive theorem provers

We present a new way to define the semantics of imperative synchronous languages by means of separating the control and the data flow. The control flow is defined by predi-cates that describe entering conditions, conditions for in-ternal moves, and termination conditions. The data flow is based on the extraction of guarded commands. This defini-tion principle can be applied to any imperative synchronous language like Esterel or some statechart variants. Follow-ing this definition principle, we have embedded our lan-guageQuartz (an Esterel variant) in the interactive theorem prover HOL. We use this embedding for formal verifica-tion (both interactive theorem proving and symbolic model checking), program analysis, reasoning about the language at a meta-level, and verified code generation (formal syn-thesis). 1