Personal tools

Certified Analyses

From PUMA Graduiertenkolleg

Revision as of 14:28, 13 February 2008 by Seidl (talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Summary

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.

Topics