Linear Functional Fixed-points

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 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.