Login
- Title:
On the Verification of Local Generic Solvers
- Author(s):
- Martin Hofmann; Aleksandr Karbyshev; Helmut Seidl
- Abstract:
- 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 two local generic fixpoint solvers RLD and RLDE, which can be applied to constraint systems x ≥ Fx, x ∈ V, over some (semi-)lattice D where the right-hand sides Fx are given as arbitrary functions implemented in some specification language. Verification of these algorithms is challenging, because they use higher-order functions and rely on side effects to track variable dependences as they are encountered dynamically during fixpoint iterations. Here, we present a correctness proof of these algorithms and show that RLDE is an exact solver while RLD is not. Proofs are formalized by means of the interactive proof assistant Coq. This paper is an extended version of [Hofmann et al. 2010a].
- Keywords:
- fixpoint algorithm; static analysis; Coq
- Year:
- 2013
- Language:
- en
BibTeX