Abstract
We define a new decidable logic for expressing and checking invariants of programs that manipulate dynamically-allocated objects via pointers and destructive pointer updates. The main feature of this logic is the ability to limit the neighborhood of a node that is reachable via a regular expression from a designated node. The logic is closed under boolean operations (entailment, negation) and has a finite model property. The key technical result is the proof of decidability.
We show how to express precondition, postconditions, and loop invariants for some interesting programs. It is also possible to express properties such as disjointness of data-structures, and low-level heap mutations. Moreover, our logic can express properties of arbitrary data-structures and of an arbitrary number of pointer fields. The latter provides a way to naturally specify postconditions that relate the fields on entry to a procedure to the fields on exit. Therefore, it is possible to use the logic to automatically prove partial correctness of programs performing low-level heap mutations.
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
Arnborg, S., Lagergren, J., Seese, D.: Easy problems for tree-decomposable graphs. J. Algorithms 12(2), 308–340 (1991)
Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 164–180. Springer, Heidelberg (2005)
Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for describing linked data structures. In: European Symp. On Programming, march 1999, pp. 2–19 (1999)
Berdine, J., Calcagno, C., O’Hearn, P.: A Decidable Fragment of Separation Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, Springer, Heidelberg (2004)
Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, Springer, Heidelberg (2005)
Bozga, M., Iosif, R.: Quantitative Verification of Programs with Lists. In: VISSAS intern. workshop, IOS Press, Amsterdam (2005)
Bozga, M., Iosif, R., Lakhnech, Y.: On logics of aliasing. In: Static Analysis Symp., pp. 344–360 (2004)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of jml tools and applications. Int. J. on Software Tools for Technology Transfer 7(3), 212–232 (2005)
Calcagno, C., Gardner, P., Hague, M.: From Separation Logic to First-Order Logic. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, Springer, Heidelberg (2005)
Calcagno, C., Yang, H., O’Hearn, P.: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, Springer, Heidelberg (2001)
Courcelle, B.: The monadic second-order logic of graphs, ii: Infinite graphs of bounded width. Mathematical Systems Theory 21(4), 187–221 (1989)
Grädel, E.: Guarded fixed point logic and the monadic theory of trees. Theoretical Computer Science 288, 129–152 (2002)
Grädel, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. Archive of Math. Logic 38, 313–354 (1999)
Grädel, E., Walukiewicz, I.: Guarded Fixed Point Logic. In: LICS 1999, IEEE, Los Alamitos (1999)
Graedel, E., Kolaitis, P., Vardi, M.: On the decision problem for two variable logic. Bulletin of Symbolic Logic (1997)
Hendren, L.: Parallelizing Programs with Recursive Data Structures. PhD thesis, Cornell Univ., Ithaca, NY (January 1990)
Hendren, L., Hummel, J., Nicolau, A.: Abstractions for recursive pointer data structures: Improving the analysis and the transformation of imperative programs. In: SIGPLAN Conf. on Prog. Lang. Design and Impl., June 1992, pp. 249–260. ACM Press, New York (1992)
Henriksen, J.G., Jensen, J., Jørgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, Springer, Heidelberg (1995)
Hoare, C.A.R.: Recursive data structures. Int. J. of Comp. and Inf. Sci. 4(2), 105–132 (1975)
Immerman, N.: Languages that capture complexity classes. SIAM Journal of Computing 16, 760–778 (1987)
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundery between decidability and undecidability of transitive closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, Springer, Heidelberg (2004)
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, Springer, Heidelberg (2004)
Ishtiaq, S.S., O’Hearn, P.W.: Bi as an assertion language for mutable data structures. In: POPL, pp. 14–26 (2001)
Klarlund, N., Schwartzbach, M.I.: Graph Types. In: POPL 1993, ACM, New York (1993)
Kuncak, V., Rinard, M.: Generalized records and spatial conjunction in role logic. In: Static Analysis Symp., Verona, Italy, August 26–28 (2004)
Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: Symp. on Princ. of Prog. Lang. (to appear, 2006)
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Static Analysis Symp., pp. 280–301 (2000)
Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: SIGPLAN Conf. on Prog. Lang. Design and Impl., pp. 221–231 (2001)
Mortimer, M.: On languages with two variables. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 21, 135–140 (1975)
Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)
Reps, T., Sagiv, M., Wilhelm, R.: Static program analysis via 3-valued logic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 15–30. Springer, Heidelberg (2004)
Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002, IEEE, Los Alamitos (2002)
Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems 20(1), 1–50 (1998)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems (2002)
Seese, D.: Interpretability and tree automata: A simple way to solve algorithmic problems on graphs closely related to trees. In: Tree Automata and Languages, pp. 83–114 (1992)
Yorsh, G., Sagiv, M., Rabinovich, A., Bouajjani, A., Meyer, A.: A logic of reachable patterns in linked data-structures. Technical report, Tel Aviv University (2005) Available at: www.cs.tau.ac.il/~gretay
Yorsh, G., Sagiv, M., Rabinovich, A., Bouajjani, A., Meyer, A.: Verification framework based on the logic of reachable patterns (in preparation, 2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yorsh, G., Rabinovich, A., Sagiv, M., Meyer, A., Bouajjani, A. (2006). A Logic of Reachable Patterns in Linked Data-Structures. In: Aceto, L., Ingólfsdóttir, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11690634_7
Download citation
DOI: https://doi.org/10.1007/11690634_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33045-5
Online ISBN: 978-3-540-33046-2
eBook Packages: Computer ScienceComputer Science (R0)