Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Verified Compilation of Space-Efficient Reversible Circuits Read chapter Read first chapter

2017 | OriginalPaper | Chapter

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic

Authors : Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin

Published in: Computer Aided Verification

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the benchmarks effectively.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter On Expansion and Resolution in CEGAR Based QBF Solving
next chapter Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts
Footnotes
1
We remark that works in [2, 9, 11, 13, 21] also discussed decision procedures for the entailment problem which is beyond the scope of this paper.
 
Literature
1.
2.
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). doi:10.​1007/​11575467_​5 CrossRef
3.
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000). doi:10.​1007/​10722167_​31 CrossRef
4.
Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227–242. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14295-6_​23 CrossRef
5.
Brotherston, J., Fuhs, C., Pérez, J.A.N., Gorogiannis, N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: CSL-LICS 2014, pp. 25:1–25:10, (2014). ACM, New York
6.
Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 68–84. Springer, Cham (2014). doi:10.​1007/​978-3-319-10936-7_​5
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 CrossRef
8.
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. SCP 77(9), 1006–1036 (2012)MATH
9.
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). doi:10.​1007/​978-3-642-23217-6_​16 CrossRef
10.
11.
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). doi:10.​1007/​978-3-319-12736-1_​17
12.
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). doi:10.​1007/​978-3-319-40229-1_​36
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). doi:10.​1007/​978-3-642-38574-2_​2 CrossRef
14.
Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM POPL, pp. 14–26, London, January 2001
15.
Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52–68. Springer, Cham (2014). doi:10.​1007/​978-3-319-08867-9_​4
16.
Le, Q.L., Sharma, A., Craciun, F., Chin, W.-N.: Towards complete specifications with an error calculus. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 291–306. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-38088-4_​20 CrossRef
17.
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). doi:10.​1007/​978-3-319-41528-4_​21
18.
Le, Q.L., Sun, J., Qin, S.: Verifying heap-manipulating programs using constrained horn clauses (technical report) (2017)
19.
Le, Q.L., Sun, J., Qin, S., Chin, W.-N.: Frame inference for inductive entailment proofs in separation logic (technical report), May 2016
20.
Le, Q.L., Tatsuta, M., Jun, S., Chin, W.-N.: A decidable fragment in separation logic with inductive predicates and arithmetic (technical report) (2017)
21.
Navarro Pérez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI 2011, pp. 556–566. ACM (2011)
22.
23.
24.
Piskac, R., Wies, T., Zufferey, D.: GRASShopper: complete heap verification with mixed specifications. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 124–139. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54862-8_​9 CrossRef
25.
26.
Qiu, X., Garg, P., Ştefănescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI, pp. 231–242 (2013). ACM, New York
27.
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: IEEE LICS, pp. 55–74 (2002)
28.
Serban, C.: A formalization of separation logic in SMT-LIB v2.5 syntax, types and semantics. Technical report, Verimag (2015) Accessed Jan 2017
29.
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). doi:10.​1007/​978-3-319-47958-3_​22 CrossRef
30.
Trinh, M.-T., Le, Q.L., David, C., Chin, W.-N.: Bi-abduction with pure properties for specification inference. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 107–123. Springer, Cham (2013). doi:10.​1007/​978-3-319-03542-0_​8 CrossRef
Metadata
Title
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Authors
Quang Loc Le
Makoto Tatsuta
Jun Sun
Wei-Ngan Chin
Copyright Year
2017
Book
Computer Aided Verification

Print ISBN: 978-3-319-63389-3

Electronic ISBN: 978-3-319-63390-9

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-63390-9_26

Premium Partner

    Image Credits