Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
Verifying a Local Generic Solver in Coq
verfasst von : Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl
Erschienen in: Static Analysis
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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
${\bf x}\sqsupseteq f_{\bf x},{\bf x}\in V$
, over some lattice
$\mathbb{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
.