Formal verification of a code generator for a synchronous language – VeriSync

The project proposed here aims at substantially improving the safety and
reliability of embedded software that is being developed in the context of a
Model Driven Engineering approach. This is achieved by formally proving the
correctness of essential transformations that a model undergoes during its
compilation to executable code.

The project is targeted at the compilation of a synchronous language to an
imperative programming language. Synchronous languages have turned out to be
an expressive formalism for embedded algorithms, and their precise semantics
make them particularly suitable for our purpose. We plan to extend the core
formalism with quantitative timing information, which is taken into account by
the transformations, so as to make the approach viable for the development of
real-time systems.

The definition of the semantics and the correctness proof of the compiler will
be carried out in the interactive proof assistant Isabelle. The compiler is
executable and will be evaluated on realistic examples.

This project is foundational in that its results are not a standalone product
which is immediately usable in an industrial context. However, the motivation
for this project has emanated from projects with major players of the embedded
sector that the partners are involved in, and the results will be fed back to
projects of industrial relevance.