Building Verified Program Analyzers in Coq: a Tutorial
David Pichardie, Inria Rennes & Harvard University, Cambridge, MA, USA.
Nowadays safety critical systems are validated through long and costly test campaigns. Static program analysis is a promising complementary technique that allows to automatically prove the absence of restricted classes of bugs. A significant example is the state-of-the-art Astrée static analyzer for C which has proven some critical safety properties for the primary flight control software of the Airbus A340 fly-by-wire system. Taking note of such a success, the next question is: should we completely remove the test campaign dedicated to the same class of bugs? If we trust the result of the analyzer, of course the answer is yes, but should we trust it? The analyzer itself can be certified by testing, but exhaustivity cannot be achieved. In this tutorial, we will show how mechanized proofs can be used to verify static analyzers themselves. This tutorial will provides a short introduction to the Coq proof assistant and will build a simple verified value analysis inside the CompCert C toolchain.