We introduce a logic of functional fixed-points. It is suitable for analyzing heap-manipulating programs and can encode several logics used for program verification with different ways of expressing reachability. While full fixed-point logic remains undecidable, several subsets admit decision procedures. In particular, for the logic of linear functional fixed-points, we develop an abstraction refinement integration of the SMT solver Z3 and a satisfiability checker for propositional linear-time temporal logic. The integration refines the temporal abstraction by generating safety formulas until the temporal abstraction is unsatisfiable or a model for it is also a model for the functional fixed-point formula. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Bjørner, N., & Hendrix, J. (2009). Linear functional fixed-points. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5643 LNCS, pp. 124–139). https://doi.org/10.1007/978-3-642-02658-4_13
Mendeley helps you to discover research relevant for your work.