2012, Max Planck Institute for Software Systems, Kaiserslautern site
Dreyer, Derek; Vafeiadis, Viktor
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.