Advertisement

Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints

  • Chong Gao
  • Taolue Chen
  • Zhilin WuEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11376)

Abstract

We identify difference-bound set constraints (DBS), an analogy of difference-bound arithmetic constraints for sets. DBS can express not only set constraints but also arithmetic constraints over set elements. We integrate DBS into separation logic with linearly compositional inductive predicates, obtaining a logic thereof where set data constraints of linear data structures can be specified. We show that the satisfiability of this logic is decidable. A crucial step of the decision procedure is to compute the transitive closure of DBS-definable set relations, to capture which we propose an extension of quantified set constraints with Presburger Arithmetic (RQSPA). The satisfiability of RQSPA is then shown to be decidable by harnessing advanced automata-theoretic techniques.

References

  1. 1.
    Bouajjani, A., Drăgoi, C., Enea, C., Sighireanu, M.: Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 167–182. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33386-6_14CrossRefzbMATHGoogle Scholar
  2. 2.
    Bozga, M., Gîrlea, C., Iosif, R.: Iterating octagons. In: TACAS, pp. 337–351 (2009)Google Scholar
  3. 3.
    Bozga, M., Iosif, R., Konecný, F.: Fast acceleration of ultimately periodic relations. In: CAV, pp. 227–242 (2010)Google Scholar
  4. 4.
    Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundam. Inf. 91(2), 275–303 (2009)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Büchi, R.J.: Weak Second-Order arithmetic and finite automata. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 6(1–6), 66–92 (1960)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Cantone, D., Cutello, V., Schwartz, J.T.: Decision problems for tarski and presburger arithmetics extended with sets. In: Börger, E., Kleine Büning, H., Richter, M.M., Schönfeld, W. (eds.) CSL 1990. LNCS, vol. 533, pp. 95–109. Springer, Heidelberg (1991).  https://doi.org/10.1007/3-540-54487-9_54CrossRefGoogle Scholar
  7. 7.
    Chin, W.-N., 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. 77(9), 1006–1036 (2012)CrossRefGoogle Scholar
  8. 8.
    Chu, D.-H., Jaffar, J., Trinh, M.-T.: Automatic induction proofs of data-structures in imperative programs. In: PLDI, pp. 457–466 (2015)Google Scholar
  9. 9.
    Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0028751CrossRefGoogle Scholar
  10. 10.
    Cristiá, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 185–201. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63046-5_12CrossRefGoogle Scholar
  11. 11.
    Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Am. Math. Soc. 98(1), 21–51 (1961)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Enea, C., Lengál, O., Sighireanu, M., Vojnar, T.: Compositional entailment checking for a fragment of separation logic. In: APLAS, pp. 314–333 (2014)Google Scholar
  13. 13.
    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, Cham (2015).  https://doi.org/10.1007/978-3-319-24953-7_7CrossRefzbMATHGoogle Scholar
  14. 14.
    Gao, C., Chen, T., Wu, Z.: Separation logic with linearly compositional inductive predicates and set data constraints (full version). http://arxiv.org/abs/1811.00699
  15. 15.
    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_36CrossRefGoogle Scholar
  16. 16.
    Halpern, J.Y.: Presburger arithmetic with unary predicates is \({\varPi }_{1}^{1}\)-complete. J. Symb. Logic 56(2), 637–642 (1991)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Horbach, M., Voigt, M., Weidenbach, C.: On the combination of the Bernays–Schönfinkel–Ramsey fragment with simple linear integer arithmetic. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 77–94. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63046-5_6CrossRefGoogle Scholar
  18. 18.
    Klaedtke, F., Rueß, H.: Monadic second-order logics with cardinalities. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 681–696. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-45061-0_54CrossRefGoogle Scholar
  19. 19.
    Konečný, F.: PTIME computation of transitive closures of octagonal relations. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 645–661. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_42CrossRefGoogle Scholar
  20. 20.
    Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 34–48. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15205-4_5CrossRefGoogle Scholar
  21. 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_21CrossRefGoogle Scholar
  22. 22.
    Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL 2011, pp. 611–622. ACM (2011)Google Scholar
  23. 23.
    Madhusudan, P., Qiu, X., Stefanescu, A.: Recursive proofs for inductive tree data-structures. In: POPL, pp. 123–136 (2012)Google Scholar
  24. 24.
    Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44978-7_10CrossRefGoogle Scholar
  25. 25.
    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).  https://doi.org/10.1007/3-540-44802-0_1CrossRefGoogle Scholar
  26. 26.
    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_54CrossRefGoogle Scholar
  27. 27.
    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_47CrossRefGoogle Scholar
  28. 28.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)Google Scholar
  29. 29.
    Seidl, H., Schwentick, T., Muscholl, A., Habermehl, P.: Counting in trees for free. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1136–1149. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27836-8_94CrossRefGoogle Scholar
  30. 30.
    Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL 2010, pp. 199–210. ACM (2010)Google Scholar
  31. 31.
    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_22CrossRefzbMATHGoogle Scholar
  32. 32.
    Voigt, M.: The Bernays–Schönfinkel–Ramsey fragment with bounded difference constraints over the reals is decidable. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 244–261. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66167-4_14CrossRefGoogle Scholar
  33. 33.
    Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 366–382. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04222-5_23CrossRefzbMATHGoogle Scholar
  34. 34.
    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_31CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.State Key Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingChina
  2. 2.University of Chinese Academy of SciencesBeijingChina
  3. 3.Department of Computer Science and Information SystemsBirkbeck, University of LondonLondonUK

Personalised recommendations