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