Sciweavers

Share
ACSD
2001
IEEE

Embedding Imperative Synchronous Languages in Interactive Theorem Provers

11 years 5 months ago
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 predicates that describe entering conditions, conditions for internal moves, and termination conditions. The data flow is based on the extraction of guarded commands. This definition principle can be applied to any imperative synchronous language like Esterel or some statechart variants. Following this definition principle, we have embedded our language Quartz (an Esterel variant) in the interactive theorem prover HOL. We use this embedding for formal verification (both interactive theorem proving and symbolic model checking), program analysis, reasoning about the language at a meta-level, and verified code generation (formal synthesis).
Klaus Schneider
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2001
Where ACSD
Authors Klaus Schneider
Comments (0)
books