Research report 2011 - Max Planck Institute for Software Systems, Kaiserslautern site

Toward the compositional verification of realistic compilers

Authors
Dreyer, Derek; Vafeiadis, Viktor
Departments
Type Systems and Functional Programming (Derek Dreyer); Software Analysis and Verification (Viktor Vafeiadis)
Summary
The field of software verification offers a rigorous methodology for specifying formally what programs are supposed to do, and for proving formally that they adhere to their specifications. The CompCert project, led by Xavier Leroy at INRIA, has demonstrated the feasibility of a particularly important application of this methodology, namely the verification of realistic optimizing compilers. However, several challenges remain in order to build verified compilers that support modular software development and multicore architectures.

For the full text, see the German version.

Go to Editor View