Verifying a local generic solver in Coq

Abstract. Fixpoint engines are the core components of program anal-ysis tools and compilers. If these tools are to be trusted, special at-tention 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 x w fx,x ∈ V, over some lattice D where the right-hand sides fx are given as arbitrary functions implemented in some specification language. The verification of this algorithm is chal-lenging, because it uses higher-order functions and relies on side effects to track variable dependences as they are encountered dynamically dur-ing fixpoint iterations. Here, we present a correctness proof of this al-gorithm which has been formalized by means of the interactive proof assistant Coq.