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 engineering tools.

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.