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)


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.


  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). 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). 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). 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). 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). Scholar
  14. 14.
    Gao, C., Chen, T., Wu, Z.: Separation logic with linearly compositional inductive predicates and set data constraints (full version).
  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). 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). 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). 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). 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). 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). 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). 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). 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). 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). 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). 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). 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). 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). 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). 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