Advertisement

Automating Separation Logic with Trees and Data

  • Ruzica Piskac
  • Thomas Wies
  • Damien Zufferey
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

Separation logic (SL) is a widely used formalism for verifying heap manipulating programs. Existing SL solvers focus on decidable fragments for list-like structures. More complex data structures such as trees are typically unsupported in implementations, or handled by incomplete heuristics. While complete decision procedures for reasoning about trees have been proposed, these procedures suffer from high complexity, or make global assumptions about the heap that contradict the separation logic philosophy of local reasoning. In this paper, we present a fragment of classical first-order logic for local reasoning about tree-like data structures. The logic is decidable in NP and the decision procedure allows for combinations with other decidable first-order theories for reasoning about data. Such extensions are essential for proving functional correctness properties. We have implemented our decision procedure and, building on earlier work on translating SL proof obligations into classical logic, integrated it into an SL-based verification tool. We successfully used the tool to verify functional correctness of tree-based data structure implementations.

Keywords

Decision Procedure Ground Term Binary Search Tree Tree Predicate 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.

References

  1. 1.
    Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 17–31. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Holík, L., Jonsson, B., Lengál, O., Trinh, C.Q., Vojnar, T.: Verification of heap manipulating programs with ordered data by extended forest automata. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 224–239. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  3. 3.
    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
  4. 4.
    Berdine, J., Calcagno, C., O’Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97–109. Springer, Heidelberg (2004)Google Scholar
  5. 5.
    Berdine, J., Calcagno, C., O’Hearn, P.W.: 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
  6. 6.
    Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory Safety for Systems-Level Code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  7. 7.
    Bouajjani, A., Drăgoi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 178–195. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    Calvanese, D., di Giacomo, G., Nardi, D., Lenzerini, M.: Reasoning in expressive description logics. In: Handbook of Automated Reasoning. Elsevier (2001)Google Scholar
  9. 9.
    Chlipala, A.: The bedrock structured programming system: Combining generative metaprogramming and hoare logic in an extensible program verifier. In: ICFP, pp. 391–402. ACM (2013)Google Scholar
  10. 10.
    Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 235–249. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  11. 11.
    de Moura, L., Bjørner, N.S.: 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
  12. 12.
    Dudka, K., Peringer, P., Vojnar, T.: Predator: A practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 372–378. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  13. 13.
    Genevès, P., Layaïda, N., Schmitt, A.: Efficient static analysis of XML paths and types. In: ACM PLDI (2007)Google Scholar
  14. 14.
    GRASShopper tool web page, http://cs.nyu.edu/wies/software/grasshopper (accessed: May 2014)
  15. 15.
    Haase, C., Ishtiaq, S., Ouaknine, J., Parkinson, M.J.: Seloger: A tool for graph-based reasoning in separation logic. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 790–795. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  16. 16.
    Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., 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
  18. 18.
    Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 21–38. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  19. 19.
    Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 756–772. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  20. 20.
    Itzhaky, S., Lahav, O., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Modular reasoning on unique heap paths via effectively propositional formulas. In: POPL (2014)Google Scholar
  21. 21.
    Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  22. 22.
    Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus (January 2001)Google Scholar
  23. 23.
    Lahiri, S.K., Qadeer, S.: Back to the future: Revisiting precise program verification using SMT solvers. In: POPL, pp. 171–182 (2008)Google Scholar
  24. 24.
    Leino, K.R.M.: Developing verified programs with dafny. In: ICSE, pp. 1488–1490. ACM (2013)Google Scholar
  25. 25.
    Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317–353 (1980)CrossRefzbMATHGoogle Scholar
  26. 26.
    Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL, pp. 611–622. ACM (2011)Google Scholar
  27. 27.
    Madhusudan, P., Qiu, X.: Efficient Decision Procedures for Heaps Using STRAND. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 43–59. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  28. 28.
    McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, pp. 21–28 (1962)Google Scholar
  29. 29.
    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
  30. 30.
    O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)Google Scholar
  31. 31.
    Pérez, J.A.N., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI, pp. 556–566. ACM (2011)Google Scholar
  32. 32.
    Piskac, R., Wies, T., Zufferey, D.: Automating Separation Logic Using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773–789. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  33. 33.
    Piskac, R., Wies, T., Zufferey, D.: GRASShopper: Complete Heap Verification with Mixed Specifications. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 124–139. Springer, Heidelberg (2014)Google Scholar
  34. 34.
    Piskac, R., Wies, T., Zufferey, D.: On automating separation logic with trees and data. Technical Report NYU Technical Report TR2014-963, NYU (2014)Google Scholar
  35. 35.
    Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI, pp. 231–242 (2013)Google Scholar
  36. 36.
    Rakamarić, Z., Bingham, J.D., 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
  37. 37.
    Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory 2(1), 57–81 (1968)CrossRefMathSciNetGoogle Scholar
  38. 38.
    Totla, N., Wies, T.: Complete instantiation-based interpolation. In: POPL. ACM (2013)Google Scholar
  39. 39.
    Wies, T., Muñiz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 476–491. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  40. 40.
    Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  41. 41.
    Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. J. Log. Algebr. Program. (2007)Google Scholar
  42. 42.
    Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: PLDI, pp. 349–361. ACM (2008)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Ruzica Piskac
    • 1
  • Thomas Wies
    • 2
  • Damien Zufferey
    • 3
  1. 1.Yale UniversityUSA
  2. 2.New York UniversityUSA
  3. 3.MIT CSAILUSA

Personalised recommendations