From PUMA Graduiertenkolleg
Program analyses and optimizations which are meant to increase the reliability and/or effficiency of code should themselves be provably correct. The idea of this project therefore is to apply verification techniques to the implementation of analyzers. By that, we contribute to the realization of verified compilers. In general, though, we expect that in general strict quality criteria will be applied to analysis tools to be used for the certification of other programs such that the enhanced verification effort appears justified.