TY - GEN
T1 - Verifying a local generic solver in Coq
AU - Hofmann, Martin
AU - Karbyshev, Aleksandr
AU - Seidl, Helmut
PY - 2010
Y1 - 2010
N2 - 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 x ⊇ fx, x ∈ V, over some lattice D where the right-hand sides f x 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.
AB - 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 x ⊇ fx, x ∈ V, over some lattice D where the right-hand sides f x 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.
UR - http://www.scopus.com/inward/record.url?scp=78149238250&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-15769-1_21
DO - 10.1007/978-3-642-15769-1_21
M3 - Conference contribution
AN - SCOPUS:78149238250
SN - 3642157688
SN - 9783642157684
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 340
EP - 355
BT - Static Analysis - 17th International Symposium, SAS 2010, Proceedings
T2 - 17th International Static Analysis Symposium, SAS 2010
Y2 - 14 September 2010 through 16 September 2010
ER -