Erroneous and buggy software dramatically increases the cost of software
developement cycles, the maintenance phase and even minor bugs often spoil
the confidence in a software system. Software testing is one method to
improve software reliability but especially the correctness of safety critical
software crucially depends on the correctness of the underlying software
Adequate software engineering methods, especially formal methods, are
used to support the correct construction of programs in high level programming
languages. Compilers are used to transform those programs into binary executable
code on concrete hardware processors. Thus, compilers themselves are used
as tools in the process of correct construction and implementation of software.
The correctness of the entire process crucially depends on compiler correctness.
The aim of the VERIFIX project is the construction of mathematically
correct compilers, which includes both the development of formal methods
for specification and implementation of a compiler, and also the implementation
of concrete compilers and development tools. Our approach is relevant for
industrial purposes, because our constraints are very practical: To deal
with practically relevant imperative languages and to push usability and
efficiency to the foreground.