Program Verification with Separation Logic | SpringerLink
Skip to main content
Springer Nature Link
Log in

Program Verification with Separation Logic

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2018)

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

Included in the following conference series:

  • 606 Accesses

Abstract

Separation Logic is a framework for the development of modular program analyses for sequential, inter-procedural and concurrent programs. The first part of the paper introduces Separation Logic first from a historical, then from a program verification perspective. Because program verification eventually boils down to deciding logical queries such as the validity of verification conditions, the second part is dedicated to a survey of decision procedures for Separation Logic, that stem from either SMT, proof theory or automata theory. Incidentally we address issues related to decidability and computational complexity of such problems, in order to expose certain sources of intractability.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Notes

  1. 1.

    We use the term “reasoning” in general, not necessarily push-button automated decision.

  2. 2.

    The second case \(\mathsf {emp}\wedge x\approx y \vdash \exists u ~.~ x \mapsto u * \mathsf {ls}(u,y) \vee \mathsf {emp}\wedge x\approx y\) is trivial and omitted for clarity.

References

  1. Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M.I., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 411–425. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54830-7_27

    Chapter  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  3. Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178–192. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_22

    Chapter  Google Scholar 

  4. 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). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  5. Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005). https://doi.org/10.1007/11575467_5

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  7. Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 131–146. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_12

    Chapter  MATH  Google Scholar 

  8. Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Heidelberg (1997)

    Book  Google Scholar 

  9. Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 350–367. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35182-2_25

    Chapter  Google Scholar 

  10. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282. ACM (1979)

    Google Scholar 

  11. 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). https://doi.org/10.1007/978-3-642-20398-5_33

    Chapter  Google Scholar 

  12. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Footprint analysis: a shape analysis that discovers preconditions. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 402–418. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74061-2_25

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  14. Calcagno, C., Gardner, P., Hague, M.: From separation logic to first-order logic. In: Sassone, V. (ed.) FoSSaCS 2005. LNCS, vol. 3441, pp. 395–409. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31982-5_25

    Chapter  Google Scholar 

  15. Chu, D.-H., Jaffar, J., Trinh, M.-T.: Automatic induction proofs of data-structures in imperative programs. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 457–466. ACM, New York (2015)

    Google Scholar 

  16. Courcelle, B.: The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990)

    Article  MathSciNet  Google Scholar 

  17. 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). https://doi.org/10.1007/3-540-45294-X_10

    Chapter  Google Scholar 

  18. Echenim, M., Iosif, R., Peltier, N.: The complexity of prenex separation logic with one selector. CoRR, abs/1804.03556 (2018)

    Google Scholar 

  19. Echenim, M., Iosif, R., Peltier, N.: On the expressive completeness of bernays-schönfinkel-ramsey separation logic. CoRR, abs/1802.00195 (2018)

    Google Scholar 

  20. Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19–32 (1967)

    Google Scholar 

  21. Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–101 (1987)

    Article  MathSciNet  Google Scholar 

  22. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  Google Scholar 

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

    Article  Google Scholar 

  24. 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 

  25. 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 

  26. O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symb. Log. 5(2), 215–244 (1999)

    Article  MathSciNet  Google Scholar 

  27. O’Hearn, P.W., Reynolds, J.C., 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). https://doi.org/10.1007/3-540-44802-0_1

    Chapter  Google Scholar 

  28. O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. SIGPLAN Not. 39(1), 268–280 (2004)

    Article  Google Scholar 

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

    Google Scholar 

  30. 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 

  31. Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 244–261. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_16

    Chapter  Google Scholar 

  32. Sighireanu, M., Cok, D.: Report on sl-comp 2014. J. Satisfiability Boolean Model. Comput. 1 (2014)

    Google Scholar 

  33. Serban, C.: Inductor: an entailment checker for inductive systems (2017). https://github.com/cristina-serban/inductor

Download references

Author information

Authors and Affiliations

  1. CNRS/VERIMAG/Université Grenoble Alpes, Grenoble, France

    Radu Iosif

Authors
  1. Radu Iosif
    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. University of Málaga, Málaga, Spain

    María del Mar Gallardo

  2. University of Málaga, Málaga, Spain

    Pedro Merino

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Iosif, R. (2018). Program Verification with Separation Logic. In: Gallardo, M., Merino, P. (eds) Model Checking Software. SPIN 2018. Lecture Notes in Computer Science(), vol 10869. Springer, Cham. https://doi.org/10.1007/978-3-319-94111-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94111-0_3

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation