Skip to main content
SpringerLink
Log in

Compositional Satisfiability Solving in Separation Logic

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

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

Abstract

We introduce a novel decision procedure to the satisfiability problem in array separation logic combined with general inductively defined predicates and arithmetic. Our proposal differentiates itself from existing works by solving satisfiability through compositional reasoning. First, following Fermat’s method of infinite descent, it infers for every inductive definition a “base” that precisely characterises the satisfiability. It then utilises the base to derive such a base for any formula where these inductive predicates reside in. Especially, we identify an expressive decidable fragment for the compositionality. We have implemented the proposal in a tool and evaluated it over challenging problems. The experimental results show that the compositional satisfiability solving is efficient and our tool is effective and efficient when compared with existing solvers.

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 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.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

Similar content being viewed by others

References

  1. Barrett, C., Kroening, D., Melham, T.: Problem solving for the 21st century: efficient solver for satisfiability modulo theories. In: Knowledge Transfer Report, Technical report 3. London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering, June 2014

    Google Scholar 

  2. Bel’tyukov, A.P.: Decidability of the universal theory of natural numbers with addition and divisibility. J. Sov. Math. 14(5), 1436–1444 (1980)

    Article  Google Scholar 

  3. 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). https://doi.org/10.1007/978-3-540-30538-5_9

    Chapter  MATH  Google Scholar 

  4. Bozga, M., Iosif, R.: On decidability within the arithmetic of addition and divisibility. In: Sassone, V. (ed.) FoSSaCS 2005. LNCS, vol. 3441, pp. 425–439. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31982-5_27

    Chapter  MATH  Google Scholar 

  5. Brotherston, J., Fuhs, C., Gorogiannis, N., Pérez, J.N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of CSL-LICS. ACM (2014)

    Google Scholar 

  6. Brotherston, J., Gorogiannis, N., Kanovich, M.: Biabduction (and related problems) in array separation logic. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 472–490. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_29

    Chapter  Google Scholar 

  7. Brotherston, J., Kanovich, M.: On the complexity of pointer arithmetic in separation logic. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 329–349. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02768-1_18

    Chapter  Google Scholar 

  8. Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_1

    Chapter  Google Scholar 

  9. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011)

    Article  MathSciNet  Google Scholar 

  10. Chin, W.-N., Gherghina, C., Voicu, R., Le, Q.L., Craciun, F., Qin, S.: A specialization calculus for pruning disjunctive predicates to support verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 293–309. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_23

    Chapter  Google Scholar 

  11. 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). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  12. Echenim, M., Iosif, R., Peltier, N.: The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains. In: Bojańczyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 242–259. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17127-8_14

    Chapter  MATH  Google Scholar 

  13. Enea, C., Lengál, O., Sighireanu, M., Vojnar, T.: Compositional entailment checking for a fragment of separation logic. Formal Meth. Syst. Des. 51(3), 575–607 (2017). https://doi.org/10.1007/s10703-017-0289-4

    Article  MATH  Google Scholar 

  14. Gu, X., Chen, T., Wu, Z.: A complete decision procedure for linearly compositional separation logic with data constraints. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 532–549. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_36

    Chapter  Google Scholar 

  15. Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding entailments in inductive separation logic with tree automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 201–218. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11936-6_15

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  17. Jansen, C., Katelaan, J., Matheja, C., Noll, T., Zuleger, F.: Unified reasoning about robustness properties of symbolic-heap separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 611–638. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54434-1_23

    Chapter  Google Scholar 

  18. Katelaan, J., Jovanović, D., Weissenbacher, G.: A separation logic with data: small models and automation. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 455–471. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_30

    Chapter  Google Scholar 

  19. Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52–68. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_4

    Chapter  Google Scholar 

  20. Le, Q.L., He, M.: A decision procedure for string logic with quadratic equations, regular expressions and length constraints. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 350–372. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02768-1_19

    Chapter  Google Scholar 

  21. Le, Q.L., Sun, J., Chin, W.-N.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 382–404. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_21

    Chapter  Google Scholar 

  22. Le, Q.L., Sun, J., Qin, S.: Frame inference for inductive entailment proofs in separation logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 41–60. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_3

    Chapter  Google Scholar 

  23. Le, Q.L., Tatsuta, M., Sun, J., Chin, W.-N.: A decidable fragment in separation logic with inductive predicates and arithmetic. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 495–517. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_26

    Chapter  Google Scholar 

  24. Lipshitz, L.: The diophantine problem for addition and divisibility. Trans. Am. Math. Soc. 235, 271–283 (1978)

    Article  MathSciNet  Google Scholar 

  25. Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: Proceedings of the 38th Annual Symposium on Principles of Programming Languages, POPL 2011, New York, NY, USA, 2011, pp. 611–622. ACM (2011)

    Google Scholar 

  26. 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). https://doi.org/10.1007/11513988_47

    Chapter  Google Scholar 

  27. Pére, J.A.N., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, New York, NY, USA, 2011, pp. 556–566. Association for Computing Machinery (2011)

    Google Scholar 

  28. Navarro Pérez, J.A., Rybalchenko, A.: Separation logic modulo theories. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 90–106. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03542-0_7

    Chapter  Google Scholar 

  29. Pham, L.H., Le, Q.L., Phan, Q.-S., Sun, J.: Concolic testing heap-manipulating programs. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 442–461. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_27

    Chapter  Google Scholar 

  30. Pham, L.H., Le, Q.L., Phan, Q.-S., Sun, J., Qin, S.: Testing heap-based programs with java starfinder. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceedings, ICSE 2018, New York, NY, USA, 2018, pp. 268–269. ACM (2018)

    Google Scholar 

  31. Pham, L.H., Le, Q.L., Phan Q.-S., Sun, J., Qin, S.: Enhancing symbolic execution of heap-based programs with separation logic for test input generation. In: Proceeding of ATVA (2019)

    Google Scholar 

  32. 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, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_47

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-642-54862-8_9

    Chapter  Google Scholar 

  34. Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: ASIAN, pp. 331–345 (2006)

    Google Scholar 

  35. Reynolds, A., Iosif, R., Serban, C.: Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 462–482. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52234-0_25

    Chapter  Google Scholar 

  36. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74 (2002)

    Google Scholar 

  37. Sighireanu, M., Gorogiannis, N., Iosif, R.: SL-COMP 2019. https://www.irif.fr/sighirea/sl-comp/19/index.html. Accessed 15 Nov 2020

    Google Scholar 

  38. Sighireanu, M., et al.: SL-COMP: competition of solvers for separation logic. In: Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III, pp. 116–132 (2019)

    Google Scholar 

  39. Tatsuta, M., Le, Q.L., Chin, W.-N.: Decision procedure for separation logic with inductive definitions and Presburger arithmetic. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 423–443. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3_22

    Chapter  MATH  Google Scholar 

  40. Trinh, M.-T., Le, Q.L., David, C., Chin, W.-N.: Bi-abduction with pure properties for specification inference. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 107–123. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03542-0_8

    Chapter  Google Scholar 

  41. Xu, Z., Chen, T., Wu, Z.: Satisfiability of compositional separation logic with tree predicates and data constraints. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 509–527. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_31

    Chapter  Google Scholar 

Download references

Acknowledgments

The author was partially supported by the UK’s Engineering and Physical Sciences Research Council (EPSRC): Grant number EP/R006865/1.

Author information

Authors and Affiliations

  1. University College London, London, UK

    Quang Loc Le

Authors
  1. Quang Loc Le
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Quang Loc Le .

Editor information

Editors and Affiliations

  1. University of Copenhagen, Copenhagen, Denmark

    Fritz Henglein

  2. Tel Aviv University, Tel Aviv, Israel

    Sharon Shoham

  3. Technion, Haifa, Israel

    Yakir Vizel

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Le, Q.L. (2021). Compositional Satisfiability Solving in Separation Logic. In: Henglein, F., Shoham, S., Vizel, Y. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2021. Lecture Notes in Computer Science(), vol 12597. Springer, Cham. https://doi.org/10.1007/978-3-030-67067-2_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-67067-2_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-67066-5

  • Online ISBN: 978-3-030-67067-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation