Paper Info
Title
Verifying a local generic solver in coq
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 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 fx 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.
Year
DOI
Venue
2010
10.1007/978-3-642-15769-1_21
SAS
Keywords
Field
DocType
arbitrary function,constraint system,fixpoint engine,core component,local generic solver,fixpoint iteration,higher-order function,local generic fixpoint solver,interactive proof assistant,lattice d,correctness proof,side effect,higher order functions,specification language
Specification language,Programming language,Lattice (order),Computer science,Correctness,Compiler,Theoretical computer science,Program analysis,Fixed point,Solver,Proof assistant
Conference
Volume
ISSN
ISBN
6337
0302-9743
3-642-15768-8
Citations 
PageRank 
References 
8
0.50
15
Authors
3
Name
Order
Citations
PageRank
Martin Hofmann118812.61
Aleksandr Karbyshev2804.78
Helmut Seidl31468103.61