Skip to main content
SpringerLink
Log in
Book cover

Asian Symposium on Programming Languages and Systems

APLAS 2017: Programming Languages and Systems pp 169–189Cite as

Decision Procedure for Entailment of Symbolic Heaps with Arrays

  • Conference paper
  • First Online:

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

Abstract

This paper gives a decision procedure for the validity of entailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially bound. This condition is independent of the condition proposed by the CADE-2017 paper by Brotherston et al., namely, one of them does not imply the other. For improving efficiency of the decision procedure, some techniques are also presented. The main idea of the decision procedure is a novel translation of an entailment of symbolic heaps into a formula in Presburger arithmetic, and to combine it with an external SMT solver. This paper also gives experimental results by an implementation, which shows that the decision procedure works efficiently enough to use.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    https://github.com/DaisukeKimura/slar.

References

  1. Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., 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  Google Scholar 

  2. 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  Google Scholar 

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

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

    Chapter  Google Scholar 

  5. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_28

    Chapter  Google Scholar 

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

    Google Scholar 

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

  8. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Beyond reachability: shape abstraction in the presence of pointer arithmetic. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 182–203. Springer, Heidelberg (2006). https://doi.org/10.1007/11823230_13

    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), 1–66 (2011)

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  11. Enea, C., Saveluc, V., Sighireanu, M.: Compositional invariant checking for overlaid and nested linked lists. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 129–148. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_9

    Chapter  Google Scholar 

  12. 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, Cham (2014). https://doi.org/10.1007/978-3-319-12736-1_17

    Google Scholar 

  13. 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). https://doi.org/10.1007/978-3-642-38574-2_2

    Chapter  Google Scholar 

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

    Google Scholar 

  15. Kimura, D., Tatsuta, M.: Decision procedure for entailment of symbolic heaps with arrays (2017). An extended version https://arxiv.org/abs/1708.06696

  16. Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Proceedings of POPL 2008, pp. 171–182 (2008)

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

  19. Sekiguchi, T.: A practical pointer analysis for C language. Comput. Softw. 21(6), 456–471 (2004)

    Google Scholar 

  20. Tatsuta, M., Kimura, D.: Separation logic with monadic inductive definitions and implicit existentials. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 69–89. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26529-2_5

    Chapter  Google Scholar 

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

Download references

Acknowledgments

We would like to thank Prof. Xiaokang Qiu and the anonymous referees for valuable comments.

Author information

Authors and Affiliations

  1. Toho University, Chiba, Japan

    Daisuke Kimura

  2. National Institute of Informatics, Tokyo, Japan

    Makoto Tatsuta

Authors
  1. Daisuke Kimura
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Makoto Tatsuta
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Daisuke Kimura .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, Colorado, USA

    Bor-Yuh Evan Chang

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kimura, D., Tatsuta, M. (2017). Decision Procedure for Entailment of Symbolic Heaps with Arrays. In: Chang, BY. (eds) Programming Languages and Systems. APLAS 2017. Lecture Notes in Computer Science(), vol 10695. Springer, Cham. https://doi.org/10.1007/978-3-319-71237-6_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-71237-6_9

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation