Advertisement

Linear Functional Fixed-points

  • Nikolaj Bjørner
  • Joe Hendrix
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

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.

Keywords

Temporal Logic Decision Procedure Unary Predicate Linear Time Temporal Logic Temporal Abstraction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–204 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis of single-parent heaps. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 91–105. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Bjørner, N., Hendrix, J.: Linear functional fixed-points. Technical Report MSR-TR-2009-8, Microsoft Research (2009)Google Scholar
  4. 4.
    Börger, E., Grädel, Gurevich: The Classical Decision Problem. Springer, Heidelberg (1996)zbMATHGoogle Scholar
  5. 5.
    de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    Immerman, N., Rabinovich, A.M., Reps, T.W., Sagiv, S., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160–174. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: Principles of Programming Languages (POPL 2006), pp. 115–126 (2006)Google Scholar
  8. 8.
    Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: POPL, pp. 171–182. ACM, New York (2008)Google Scholar
  9. 9.
    Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, S., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 99–115. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)CrossRefzbMATHGoogle Scholar
  11. 11.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)CrossRefzbMATHGoogle Scholar
  12. 12.
    McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 476–490. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Programming Language Design and Implementation (PLDI 2001), pp. 221–231 (2001)Google Scholar
  14. 14.
    Nelson, G.: Verifying Reachability Invariants of Linked Structures. In: Principles of Programming Languages (POPL 1983), pp. 38–47 (1983)Google Scholar
  15. 15.
    Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)CrossRefzbMATHGoogle Scholar
  16. 16.
    Rakamarić, Z., Bingham, J., Hu, A.J.: An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 106–121. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Ranise, S., Zarba, C.G.: A Theory of Singly-Linked Lists and its Extensible Decision Procedure. In: SEFM 2006, pp. 206–215 (2006)Google Scholar
  18. 18.
    Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)Google Scholar
  19. 19.
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Wolper, P.: Specification and synthesis of communicating processes using an extended temporal logic. In: POPL, pp. 20–33 (1982)Google Scholar
  21. 21.
    Yorsh, G., Rabinovich, A.M., Sagiv, S., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 94–110. Springer, Heidelberg (2006)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Nikolaj Bjørner
    • 1
  • Joe Hendrix
    • 1
  1. 1.Microsoft, One Microsoft WayRedmondUSA

Personalised recommendations