Martin Hofmann, Aleksandr Karbyshev and Helmut Seidl. Verifying a Local Generic Solver in Coq. In Radhia Cousot and Matthieu Martel, editors, Static Analysis, volume 6337 of Lecture Notes in Computer Science, pages 340-355, September 2010. Springer.

Fixpoint engines are the core components of program analysis tools and compilers. If these tools are to be trusted, special attention should be paid also to the correctness of such solvers. In this paper we consider the local generic fixpoint solver RLD which can be applied to constraint systems, over some lattice where the right-hand sides are given as arbitrary functions implemented in some specification language. The verification of this algorithm is challenging, because it uses higher-order functions and relies on side effects to track variable dependences as they are encountered dynamically during fixpoint iterations. Here, we present a correctness proof of this algorithm which has been formalized by means of the interactive proof assistant Coq.

Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com