Linear Functional Fixed-points

Nikolaj Bjorner and Joe Hendrix

Abstract

We introduce a logic of functional fixed-points. It is suitable for analyzing heap-manipulating programs and can encode several of the logics recently introduced for reasoning with transitive closures. 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 labstraction 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.

Details

Publication typeTechReport
NumberMSR-TR-2009-8
> Publications > Linear Functional Fixed-points