Skip to main content
SpringerLink
Log in

Automated Mutual Explicit Induction Proof in Separation Logic

  • Conference paper
  • First Online:
FM 2016: Formal Methods (FM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9995))

Included in the following conference series:

Abstract

We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, called mutual explicit induction proof, is an instance of Noetherian induction. Specifically, we propose a novel induction principle on a well-founded relation of separation logic model, and follow the explicit induction methods to implement this principle as inference rules, so that it can be easily integrated into a deductive system. We also support mutual induction, a natural feature of implicit induction, where the goal entailment and other entailments derived during the proof search can be used as hypotheses to prove each other. We have implemented a prototype prover and evaluated it on a benchmark of handcrafted entailments as well as benchmarks from a separation logic competition.

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.

    Note that for the simplicity of presenting the motivating example, we have removed the sort \(\iota \) from the SL singleton heap predicate denoting the data structure \(\mathtt {node}\).

  2. 2.

    We exclude the set of invalid entailments because some evaluated proof techniques, such as [4, 10], aim to only prove validity of entailments.

  3. 3.

    Available at https://github.com/mihasighi/smtcomp14-sl/tree/master/bench.

  4. 4.

    The full benchmark is available at http://loris-5.d2.comp.nus.edu.sg/songbird/.

  5. 5.

    We do not list other provers in Fig. 12 as they cannot prove any problems in slrd_ind.

References

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

    Chapter  Google Scholar 

  2. 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). doi:10.1007/11575467_5

    Chapter  Google Scholar 

  3. Bozga, M., Iosif, R., Perarnau, S.: Quantitative separation logic and programs with lists. J. Autom. Reason. 45(2), 131–156 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  4. 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). doi:10.1007/978-3-642-22438-6_12

    Chapter  Google Scholar 

  5. Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 68–84. Springer, Heidelberg (2014). doi:10.1007/978-3-319-10936-7_5

    Google Scholar 

  6. Brotherston, J., Gorogiannis, N., Kanovich, M.I., Rowe, R.: Model checking for symbolic-heap separation logic with inductive predicates. In: Symposium on Principles of Programming Languages (POPL), pp. 84–96 (2016)

    Google Scholar 

  7. 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). doi:10.1007/978-3-642-35182-2_25

    Chapter  Google Scholar 

  8. Bundy, A.: The automation of proof by mathematical induction. In: Handbook of Automated Reasoning, vol. 2, pp. 845–911 (2001)

    Google Scholar 

  9. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Symposium on Principles of Programming Languages (POPL), pp. 289–300 (2009)

    Google Scholar 

  10. Chin, W., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. (SCP) 77(9), 1006–1036 (2012)

    Article  MATH  Google Scholar 

  11. Chu, D., Jaffar, J., Trinh, M.: Automatic induction proofs of data-structures in imperative programs. In: Conference on Programming Language Design and Implementation (PLDI), pp. 457–466 (2015)

    Google Scholar 

  12. 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). doi:10.1007/978-3-642-23217-6_16

    Chapter  Google Scholar 

  13. Enea, C., Lengál, O., Sighireanu, M., Vojnar, T.: Compositional entailment checking for a fragment of separation logic. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 314–333. Springer, Heidelberg (2014). doi:10.1007/978-3-319-12736-1_17

    Google Scholar 

  14. Enea, C., Sighireanu, M., Wu, Z.: On automated lemma generation for separation logic with inductive definitions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 80–96. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24953-7_7

    Chapter  Google Scholar 

  15. Infer: A tool to detect bugs in Android and iOS apps before they ship. http://fbinfer.com/. Accessed 27 May 2016

  16. Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 21–38. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_2

    Chapter  Google Scholar 

  17. 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, Heidelberg (2014). doi:10.1007/978-3-319-11936-6_15

    Google Scholar 

  18. 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, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_4

    Google Scholar 

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

    Chapter  Google Scholar 

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

  21. Nguyen, H.H., David, C., Qin, S., 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). doi:10.1007/978-3-540-69738-1_18

    Chapter  Google Scholar 

  22. 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). doi:10.1007/3-540-44802-0_1

    Chapter  Google Scholar 

  23. Pérez, J.A.N., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: Conference on Programming Language Design and Implementation (PLDI), pp. 556–566 (2011)

    Google Scholar 

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

    Chapter  Google Scholar 

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

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

  27. Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: Conference on Programming Language Design and Implementation (PLDI), pp. 231–242 (2013)

    Google Scholar 

  28. Reynolds, J.C.: An introduction to separation logic - Lecture Notes for the PhD Fall School on Logics and Semantics of State, Copenhagen (2008). http://www.cs.cmu.edu/ jcr/copenhagen08.pdf. Accessed 20 Jan 2016

  29. Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Millennial Perspectives in Computer Science, Palgrave, pp. 303–321 (2000)

    Google Scholar 

  30. Reynolds, J.C.: Separation Logic: A logic for shared mutable data structures. In: Symposium on Logic in Computer Science (LICS), pp. 55–74 (2002)

    Google Scholar 

  31. Sighireanu, M., Cok, D.R.: Report on SL-COMP 2014. J. Satisf. Boolean Model. Comput. 9, 173–186 (2016)

    MathSciNet  Google Scholar 

  32. Ta, Q.T., Le, T.C., Khoo, S.C., Chin, W.N.: Automated mutual explicit induction proof in separation logic. arXiv:1609.00919 (2016)

Download references

Acknowledgement

We would like to thank the anonymous reviewers for their valuable and helpful feedback. The first author would like to thank Dr. James Brotherston for the useful discussion about the cyclic proof. This work has been supported by NUS Research Grant R-252-000-553-112. Ton Chanh and Wei-Ngan are partially supported by MoE Tier-2 grant MOE2013-T2-2-146.

Author information

Authors and Affiliations

  1. School of Computing, National University of Singapore, Singapore, Singapore

    Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo & Wei-Ngan Chin

Authors
  1. Quang-Trung Ta
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ton Chanh Le
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Siau-Cheng Khoo
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Wei-Ngan Chin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Quang-Trung Ta .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

  2. US Naval Research Laboratory, Washington, District of Columbia, USA

    Constance Heitmeyer

  3. ISTI-CNR, Pisa, Italy

    Stefania Gnesi

  4. University of Cyprus, Nicosia, Cyprus

    Anna Philippou

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Ta, QT., Le, T.C., Khoo, SC., Chin, WN. (2016). Automated Mutual Explicit Induction Proof in Separation Logic. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_40

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48989-6_40

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48988-9

  • Online ISBN: 978-3-319-48989-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation