Skip to main content
SpringerLink
Log in

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10145))

Abstract

Separation Logic (\(\mathsf {SL}\)) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order \(\mathsf {SL}\) restricted to the Bernays-Schönfinkel-Ramsey quantifier prefix \(\exists ^*\forall ^*\), where the quantified variables range over the set of memory locations. When this set is uninterpreted (has no associated theory) the fragment is PSPACE-complete, which matches the complexity of the quantifier-free fragment [7]. However, \(\mathsf {SL}\) becomes undecidable when the quantifier prefix belongs to \(\exists ^*\forall ^*\exists ^*\) instead, or when the memory locations are interpreted as integers with linear arithmetic constraints, thus setting a sharp boundary for decidability within \(\mathsf {SL}\). We have implemented a decision procedure for the decidable fragment of \(\exists ^*\forall ^*\mathsf {SL}\) as a specialized solver inside a DPLL(T) architecture, within the CVC4 SMT solver. The evaluation of our implementation was carried out using two sets of verification conditions, produced by (i) unfolding inductive predicates, and (ii) a weakest precondition-based verification condition generator. Experimental data shows that automated quantifier instantiation has little overhead, compared to manual model-based instantiation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Strictly speaking, the Bernays-Schönfinkel-Ramsey class refers to the \(\exists ^*\forall ^*\) fragment of first-order logic with equality and predicate symbols, but no function symbols [17].

  2. 2.

    By writing \(\mathcal {I}[\sigma \leftarrow S]\) we ensure that all variables of sort \(\sigma \) are mapped by \(\mathcal {I}\) to elements of S.

  3. 3.

    If \(\mathsf {x}_1 \mapsto (\mathsf {x}_2, \ldots , \mathsf {x}_n)\) and \(\mathsf {x}_1 \mapsto (\mathsf {x}'_2, \ldots , \mathsf {x}'_n)\) hold, this forces \(\mathsf {x}_i=\mathsf {x}'_i\), for all \(i=2,\ldots ,n\).

  4. 4.

    Extending the interpretation of \(\mathsf {Loc}\) to include negative integers does not make any difference for the undecidability result.

  5. 5.

    The procedure is incorporated into the master branch of the SMT solver CVC4 (https://github.com/CVC4), and can be enabled by command line parameter - -quant-epr.

  6. 6.

    Available at http://cvc4.cs.nyu.edu/web/.

  7. 7.

    The CVC4 binary and examples used in these experiments are available at http://cs.uiowa.edu/~ajreynol/VMCAI2017-seplog-epr.

References

  1. Albargouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 634–660. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46669-8_26

    Chapter  Google Scholar 

  2. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  3. Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21–52 (2006)

    Article  MATH  Google Scholar 

  4. Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106–137 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  5. Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Logic Comput. 21(6), 1177–1216 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  6. Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 459–465. Springer, Heidelberg (2011). doi:10.1007/978-3-642-20398-5_33

    Chapter  Google Scholar 

  7. Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001). doi:10.1007/3-540-45294-X_10

    Chapter  Google Scholar 

  8. Demri, S., Deters, M.: Two-variable separation logic and its inner circle. ACM Trans. Comput. Logic 16(2) (2015). Article no. 15

    Google Scholar 

  9. Demri, S., Galmiche, D., Larchey-Wendling, D., Méry, D.: Separation logic with one quantified variable. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.É., Vereshchagin, N.K. (eds.) CSR 2014. LNCS, vol. 8476, pp. 125–138. Springer, Heidelberg (2014). doi:10.1007/978-3-319-06686-8_10

    Google Scholar 

  10. 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). doi:10.1007/978-3-642-22110-1_29

    Chapter  Google Scholar 

  11. Galmiche, D., Méry, D.: Tableaux and resource graphs for separation logic. J. Logic Comput. 20(1), 189–231 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  12. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Berlin (2004). doi:10.1007/978-3-540-27813-9_14

    Chapter  Google Scholar 

  13. Ge, Y., Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_25

    Chapter  Google Scholar 

  14. Halpern, J.Y.: Presburger arithmetic with unary predicates is \(\pi ^1_1\) complete. J. Symbolic Logic 56(2), 637–642 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  15. Ishtiaq, S.S., O’Hearn, P.W.: Bi as an assertion language for mutable data structures. ACM SIGPLAN Not. 36, 14–26 (2001)

    Article  MATH  Google Scholar 

  16. Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: Proceedings of 4th International Joint Conference on Automated Reasoning, IJCAR 2008, Sydney, Australia, 12–15 August 2008, pp. 292–298 (2008)

    Google Scholar 

  17. Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317–353 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  18. Matiyasevich, Y.: Enumerable sets are diophantine. J. Sovietic Math. 11, 354–358 (1970)

    MATH  Google Scholar 

  19. Nguyen, H.H., Chin, W.-N.: Enhancing program verification with lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 355–369. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70545-1_34

    Chapter  Google Scholar 

  20. Piskac, R., de Moura, L.M., Bjørner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning 44(4), 401–424 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  21. 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). doi:10.1007/978-3-642-39799-8_54

    Chapter  Google Scholar 

  22. Piskac, R., Wies, T., Zufferey, D.: Automating Separation Logic with Trees and Data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711–728. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_47

    Google Scholar 

  23. Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counter example-guided quantifier instantiation for synthesis in SMT. In: Proceedings of Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, 18–24 July 2015, Part II, pp. 198–216 (2015)

    Google Scholar 

  24. Reynolds, A., Iosif, R., Serban, C.: Reasoning in the Bernays-Schoenfinkel-Ramsey fragment of separation logic. CoRR abs/1610.04707 (2016). http://arxiv.org/abs/1610.04707

  25. Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Proceedings of 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, Chiba, Japan, 17–20 October 2016, pp. 244–261 (2016)

    Google Scholar 

  26. Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640–655. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_42

    Chapter  Google Scholar 

  27. Sighireanu, M., Cok, D.: Report on SL-COMP 2014. J. Satisfiability Boolean Model. Comput. 1 (2014)

    Google Scholar 

  28. Toubhans, A., Chang, B.-Y.E., Rival, X.: An abstract domain combinator for separately conjoining memory abstractions. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 285–301. Springer, Heidelberg (2014). doi:10.1007/978-3-319-10936-7_18

    Google Scholar 

  29. Voigt, M., Weidenbach, C.: Bernays-Schönfinkel-Ramsey with simple bounds is nexptime-complete. CoRR abs/1501.07209 (2015)

    Google Scholar 

  30. Yang, H.: Local reasoning for stateful programs. Ph.D. thesis, University of Illinois at Urbana-Champaign (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The University of Iowa, Iowa City, USA

    Andrew Reynolds

  2. Verimag/CNRS/Université de Grenoble Alpes, Grenoble, France

    Radu Iosif & Cristina Serban

Authors
  1. Andrew Reynolds
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Radu Iosif
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cristina Serban
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Radu Iosif .

Editor information

Editors and Affiliations

  1. IRIF, Université Paris Diderot, Paris, France

    Ahmed Bouajjani

  2. VERIMAG, CNRS & Université Grenoble Alpes, Grenoble, France

    David Monniaux

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Reynolds, A., Iosif, R., Serban, C. (2017). Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. In: Bouajjani, A., Monniaux, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2017. Lecture Notes in Computer Science(), vol 10145. Springer, Cham. https://doi.org/10.1007/978-3-319-52234-0_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-52234-0_25

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-52233-3

  • Online ISBN: 978-3-319-52234-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation