Abstract
This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic (\(\mathsf {SL}\)) interpreted over heaplets with data elements ranging over a parametric multi-sorted (possibly infinite) domain. The algorithm uses a combination of theories and is used as a specialized solver inside a DPLL(T) architecture. A prototype was implemented within the CVC4 SMT solver. Preliminary evaluation suggests the possibility of using this procedure as a building block of a more elaborate theorem prover for \(\mathsf {SL}\) with inductive predicates, or as back-end of a bounded model checker for programs with low-level pointer and data manipulations.
R. Iosif and C. Serban—Supported by the French National Research Agency project VECOLIB (ANR-14-CE28-0018).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
For brevity, we may write \(p( \mathbf t )\) as shorthand for \(p( \mathbf t ) \approx \top \), where p is a function into \(\mathsf {Bool}\).
- 2.
Take for instance \(\phi \) as \(x \mapsto 1\) and \(\varphi \) as \(y \mapsto 2\).
- 3.
We denote by \({F}\!\!\downarrow _{{D}}\) the restriction of the function F to the domain \(D\subseteq \mathrm {dom}(F)\).
- 4.
Non-constant Skolem symbols k introduced by the procedure may be treated as uninterpreted functions. Constraints of the form \(k \subseteq S_1 \times S_2\) are translated to \(\bigwedge _{c \in S_1} k( c ) \in S_2\). Furthermore, the domain of k may be restricted to the set \(\{ c^\mathcal {I}\mid c \in S_1 \}\) in models \(\mathcal {I}\) found in Steps 1 and 2 of the procedure. This restriction comes with no loss of generality since, by construction of \((\varphi \triangleleft [\ell ,\mathsf {pt},C])\!\!\Downarrow \), k is applied only to terms occurring in \(S_1\).
- 5.
These functions are over the \(\mathsf {Bool}\) sort. We refer to these functions as taking formulae as input, where formulae may be cast to terms of sort \(\mathsf {Bool}\) through use of an if-then-else construct.
- 6.
Available at http://cvc4.cs.nyu.edu/web/.
- 7.
The CVC4 binary and examples used in these experiments are available at http://cvc4.cs.nyu.edu/papers/ATVA2016-seplog/.
References
Bansal, K.: Decision procedures for finite sets with cardinality and local theory extensions. Ph.D. thesis, New York University (2016)
Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV 2011, pp. 171–177 (2011)
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB 2.5 standard. Technical report, The University of Iowa (2015). http://smt-lib.org/
Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178–192. Springer, Heidelberg (2007)
Bjørner, N., Janota, M.: Playing with quantified satisfaction. In: LPAR 2015. EPIC, vol. 35, pp. 15–27 (2015)
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)
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)
Calcagno, C., Gardner, P., Hague, M.: From separation logic to first-order logic. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 395–409. Springer, Heidelberg (2005)
Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001)
Enea, C., Sighireanu, M., Wu, Z.: On automated lemma generation for separation logic with inductive definitions. In: Finkbeiner, B., et al. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 80–96. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24953-7_7
Galmiche, D., Méry, D.: Tableaux and resource graphs for separation logic. J. Logic Comput. 20(1), 189–231 (2010)
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, Heidelberg (2004)
Ge, Y., de 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)
Iosif, R., Rogalewicz, A., Vojnar, T.: Slide: Separation logic with inductive definitions. http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/
Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. ACM SIGPLAN Not. 36, 14–26 (2001)
Navarro Pérez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. ACM SIGPLAN Not. 46(6), 556–566 (2011)
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)
Piskac, R., Wies, T., Zufferey, D., 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)
Reynolds, A., Deters, M., Kuncak, V., Barrett, C.W., Tinelli, C.: Counterexample guided quantifier instantiation for synthesis in CVC4. In: CAV 2015, pp. 198–216 (2015)
Reynolds, A., King, T., Kuncak, V.: An instantiation-based approach for solving quantified linear arithmetic. CoRR abs/1510.02642 (2015)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science, LICS 2002, pp. 55–74 (2002)
Sighireanu, M., Cok, D.: Report on SL-COMP 2014. J. Satisf. Boolean Modeling Comput. 1, 173–186 (2014)
Piskac, R., Kuncak, V., Suter, P., Steiger, R., Kuncak, V.: Sets with cardinality constraints in satisfiability modulo theories. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 403–418. Springer, Heidelberg (2011)
Yang, H.: Local reasoning for stateful programs. Ph.D. thesis, University of Illinois at Urbana-Champaign (2001)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Reynolds, A., Iosif, R., Serban, C., King, T. (2016). A Decision Procedure for Separation Logic in SMT. In: Artho, C., Legay, A., Peled, D. (eds) Automated Technology for Verification and Analysis. ATVA 2016. Lecture Notes in Computer Science(), vol 9938. Springer, Cham. https://doi.org/10.1007/978-3-319-46520-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-46520-3_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-46519-7
Online ISBN: 978-3-319-46520-3
eBook Packages: Computer ScienceComputer Science (R0)