×

Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic. (English) Zbl 1484.68104

Bouajjani, Ahmed (ed.) et al., Verification, model checking, and abstract interpretation. 18th international conference, VMCAI 2017, Paris, France, January 15–17, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10145, 462-482 (2017).
Summary: Separation logic (\(\mathsf {SL}\)) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order \(\mathsf {SL}\) restricted to the Bernays-Schönfinkel-Ramsey quantifier prefix \(\exists ^*\forall^*\), where the quantified variables range over the set of memory locations. When this set is uninterpreted (has no associated theory) the fragment is PSPACE-complete, which matches the complexity of the quantifier-free fragment [C. Calcagno et al., Lect. Notes Comput. Sci. 2245, 108–119 (2001; Zbl 1052.68590)]. However, \(\mathsf {SL}\) becomes undecidable when the quantifier prefix belongs to \(\exists ^*\forall ^*\exists ^*\) instead, or when the memory locations are interpreted as integers with linear arithmetic constraints, thus setting a sharp boundary for decidability within \(\mathsf {SL}\). We have implemented a decision procedure for the decidable fragment of \(\exists ^*\forall ^*\mathsf {SL}\) as a specialized solver inside a DPLL(\(T\)) architecture, within the CVC4 SMT solver. The evaluation of our implementation was carried out using two sets of verification conditions, produced by (i) unfolding inductive predicates, and (ii) a weakest precondition-based verification condition generator. Experimental data shows that automated quantifier instantiation has little overhead, compared to manual model-based instantiation.
For the entire collection see [Zbl 1355.68009].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science

Citations:

Zbl 1052.68590

Software:

Infer; CVC4; iProver; Predator
PDFBibTeX XMLCite
Full Text: DOI arXiv HAL

References:

[1] Albargouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 634–660. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46669-8_26 · Zbl 1335.68040 · doi:10.1007/978-3-662-46669-8_26
[2] 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). doi: 10.1007/978-3-642-22110-1_14 · Zbl 05940712 · doi:10.1007/978-3-642-22110-1_14
[3] Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21–52 (2006) · Zbl 05421296 · doi:10.1142/S0218213006002552
[4] Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106–137 (2012) · Zbl 1262.03051 · doi:10.1016/j.ic.2011.12.003
[5] Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Logic Comput. 21(6), 1177–1216 (2011) · Zbl 1242.03084 · doi:10.1093/logcom/exq052
[6] 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). doi: 10.1007/978-3-642-20398-5_33 · Zbl 05930547 · doi:10.1007/978-3-642-20398-5_33
[7] 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). doi: 10.1007/3-540-45294-X_10 · Zbl 1052.68590 · doi:10.1007/3-540-45294-X_10
[8] Demri, S., Deters, M.: Two-variable separation logic and its inner circle. ACM Trans. Comput. Logic 16(2) (2015). Article no. 15 · Zbl 1354.03036 · doi:10.1145/2724711
[9] Demri, S., Galmiche, D., Larchey-Wendling, D., Méry, D.: Separation logic with one quantified variable. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.É., Vereshchagin, N.K. (eds.) CSR 2014. LNCS, vol. 8476, pp. 125–138. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-06686-8_10 · Zbl 1408.68036 · doi:10.1007/978-3-319-06686-8_10
[10] Dudka, K., Peringer, P., Vojnar, T.: Predator: a practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 372–378. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22110-1_29 · Zbl 05940727 · doi:10.1007/978-3-642-22110-1_29
[11] Galmiche, D., Méry, D.: Tableaux and resource graphs for separation logic. J. Logic Comput. 20(1), 189–231 (2010) · Zbl 1193.03061 · doi:10.1093/logcom/exn066
[12] Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Berlin (2004). doi: 10.1007/978-3-540-27813-9_14 · Zbl 1103.68616 · doi:10.1007/978-3-540-27813-9_14
[13] Ge, Y., Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02658-4_25 · Zbl 1242.68280 · doi:10.1007/978-3-642-02658-4_25
[14] Halpern, J.Y.: Presburger arithmetic with unary predicates is \[ \pi ^1_1 \] complete. J. Symbolic Logic 56(2), 637–642 (1991) · Zbl 0738.03017 · doi:10.2307/2274706
[15] Ishtiaq, S.S., O’Hearn, P.W.: Bi as an assertion language for mutable data structures. ACM SIGPLAN Not. 36, 14–26 (2001) · Zbl 1323.68077 · doi:10.1145/373243.375719
[16] Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: Proceedings of 4th International Joint Conference on Automated Reasoning, IJCAR 2008, Sydney, Australia, 12–15 August 2008, pp. 292–298 (2008) · Zbl 1165.68462 · doi:10.1007/978-3-540-71070-7_24
[17] Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317–353 (1980) · Zbl 0471.03034 · doi:10.1016/0022-0000(80)90027-6
[18] Matiyasevich, Y.: Enumerable sets are diophantine. J. Sovietic Math. 11, 354–358 (1970) · Zbl 0212.33401
[19] 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 · Zbl 1155.68443 · doi:10.1007/978-3-540-70545-1_34
[20] Piskac, R., de Moura, L.M., Bjørner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning 44(4), 401–424 (2010) · Zbl 1197.03011 · doi:10.1007/s10817-009-9161-6
[21] 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 · Zbl 06233076 · doi:10.1007/978-3-642-39799-8_54
[22] 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 · Zbl 06349543 · doi:10.1007/978-3-319-08867-9_47
[23] Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counter example-guided quantifier instantiation for synthesis in SMT. In: Proceedings of Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, 18–24 July 2015, Part II, pp. 198–216 (2015) · Zbl 1381.68059
[24] Reynolds, A., Iosif, R., Serban, C.: Reasoning in the Bernays-Schoenfinkel-Ramsey fragment of separation logic. CoRR abs/1610.04707 (2016). http://arxiv.org/abs/1610.04707 · Zbl 1484.68104
[25] Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Proceedings of 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, Chiba, Japan, 17–20 October 2016, pp. 244–261 (2016) · Zbl 1398.68486 · doi:10.1007/978-3-319-46520-3_16
[26] Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640–655. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39799-8_42 · Zbl 06233064 · doi:10.1007/978-3-642-39799-8_42
[27] Sighireanu, M., Cok, D.: Report on SL-COMP 2014. J. Satisfiability Boolean Model. Comput. 1 (2014)
[28] Toubhans, A., Chang, B.-Y.E., Rival, X.: An abstract domain combinator for separately conjoining memory abstractions. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 285–301. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-10936-7_18 · Zbl 06349464 · doi:10.1007/978-3-319-10936-7_18
[29] Voigt, M., Weidenbach, C.: Bernays-Schönfinkel-Ramsey with simple bounds is nexptime-complete. CoRR abs/1501.07209 (2015)
[30] Yang, H.: Local reasoning for stateful programs. Ph.D. thesis, University of Illinois at Urbana-Champaign (2001)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.