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.

PDF file

Details