Beyond Shapes: Lists with Ordered Data

  • Kshitij Bansal
  • Rémi Brochenin
  • Etienne Lozes
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)


Standard analysis on recursive data structures restrict their attention to shape properties (for instance, a program that manipulates a list returns a list), excluding properties that deal with the actual content of these structures. For instance, these analysis would not establish that the result of merging two ordered lists is an ordered list. Separation logic, one of the prominent framework for these kind of analysis, proposed a heap model that could represent data, but, to our knowledge, no predicate dealing with data has ever been integrated to the logic while preserving decidability. We establish decidability for (first-order) separation logic with a predicate that allows to compare two successive data in a list. We then consider the extension where two data in arbitrary positions may be compared, and establish the undecidability in general. We define a guarded fragment that turns out to be both decidable and sufficiently expressive to prove the preservation of the loop invariant of a standard program merging ordered lists. We finally consider the extension with the magic-wand and prove that, by constrast with the data-free case, even a very restricted use of the magic wand already introduces undecidability.


Memory Shape Order Logic Memory State Order Data Separation Logic 
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.


  1. 1.
    Berdine, J., Calcagno, C., O’Hearn, P.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: Proceedings of 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, pp. 7–16 (2006)Google Scholar
  3. 3.
    Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 517–531. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Bozga, M., Iosif, R., Lakhnech, Y.: On logics of aliasing. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 344–360. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Technical report, LSV, ENS de Cachan (2008)Google Scholar
  6. 6.
    Brochenin, R., Demri, S., Lozes, É.: On the almighty wand (To appear). In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 323–338. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    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, pp. 108–119. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  8. 8.
    Demri, S., Lazić, R., Nowak, D.: On the freeze quantifier in constraint LTL: Decidability and complexity. In: Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), Burlington, Vermont, USA, pp. 113–121. IEEE Computer Society Press, Los Alamitos (2005)CrossRefGoogle Scholar
  9. 9.
    Jensen, J., Jorgensen, M., Klarlund, N., Schwartzbach, M.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI 1997, pp. 226–236. ACM, New York (1997)Google Scholar
  10. 10.
    Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280–302. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  11. 11.
    Loginov, A., Reps, T., Sagiv, M.: Refinement-based verification for possibly-cyclic lists. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol. 4444, pp. 247–272. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Rabin, M.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 41, 1–35 (1969)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE, Los Alamitos (2002)Google Scholar
  15. 15.
    Trakhtenbrot, B.A.: The impossibility of an algorithm for the decision problem for finite models. Dokl. Akad. Nauk SSSR 70, 572–596 (1950); English translation in: AMS Transl. Ser. 2, 23(1063), 1–6Google Scholar
  16. 16.
    Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data structures. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 94–110. Springer, Heidelberg (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Kshitij Bansal
    • 1
  • Rémi Brochenin
    • 2
  • Etienne Lozes
    • 2
  1. 1.Chennai Mathematical InstituteIndia
  2. 2.LSV, ENS Cachan, CNRSFrance

Personalised recommendations