Martin Hofmann, Aleksandr Karbyshev, and Helmut Seidl (2010)

# Verifying a Local Generic Solver in Coq

In: SAS, pp. 340-355.

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.

Document Actions