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.
Chapter PDF
Similar content being viewed by others
Keywords
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
Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–204 (1994)
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)
Bjørner, N., Hendrix, J.: Linear functional fixed-points. Technical Report MSR-TR-2009-8, Microsoft Research (2009)
Börger, E., Grädel, Gurevich: The Classical Decision Problem. Springer, Heidelberg (1996)
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)
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)
Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: Principles of Programming Languages (POPL 2006), pp. 115–126 (2006)
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)
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)
Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)
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)
Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Programming Language Design and Implementation (PLDI 2001), pp. 221–231 (2001)
Nelson, G.: Verifying Reachability Invariants of Linked Structures. In: Principles of Programming Languages (POPL 1983), pp. 38–47 (1983)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
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)
Ranise, S., Zarba, C.G.: A Theory of Singly-Linked Lists and its Extensible Decision Procedure. In: SEFM 2006, pp. 206–215 (2006)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)
Wolper, P.: Specification and synthesis of communicating processes using an extended temporal logic. In: POPL, pp. 20–33 (1982)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bjørner, N., Hendrix, J. (2009). Linear Functional Fixed-points. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)