Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Disjoint Polymorphism Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

verfasst von : Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger

Erschienen in: Programming Languages and Systems

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We introduce heap automata, a formalism for automatic reasoning about robustness properties of the symbolic heap fragment of separation logic with user-defined inductive predicates. Robustness properties, such as satisfiability, reachability, and acyclicity, are important for a wide range of reasoning tasks in automated program analysis and verification based on separation logic. Previously, such properties have appeared in many places in the separation logic literature, but have not been studied in a systematic manner. In this paper, we develop an algorithmic framework based on heap automata that allows us to derive asymptotically optimal decision procedures for a wide range of robustness properties in a uniform way.
We implemented a prototype of our framework and obtained promising results for all of the aforementioned robustness properties.
Further, we demonstrate the applicability of heap automata beyond robustness properties. We apply our algorithmic framework to the model checking and the entailment problem for symbolic-heap separation logic.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Verified Characteristic Formulae for CakeML
Nächstes Kapitel Proving Linearizability Using Partial Orders
Fußnoten
1
Since \(\mathbf {x}_{i}^{}\!\left[ 0\right] \) is just a shortcut and not a proper variable, \(\Vert \mathbf {x}_{i}^{}\Vert \) refers to the number of variables in \(\mathbf {x}_{i}^{}\) apart from \(\mathbf {x}_{i}^{}\!\left[ 0\right] \).
 
2
We assume a reasonable function \(\Vert .\Vert \) assigning a size to SIDs, symbolic heaps, unfolding trees, etc. For instance, the size \(\Vert \varPhi \Vert \) of an SID \(\varPhi \) is given by the product of its number of rules and the size of the largest symbolic heap contained in any rule.
 
3
Sometimes this property is also defined by requiring that each existentially quantified variable is “eventually allocated”  [26].
 
4
The definite points-to relation \(\mapsto _{\tau }\) was defined at the beginning of Sect. 4.
 
5
Note that a variable may be reachable from different program variables in different unfoldings as garbage-freedom is formally defined as a set of reduced symbolic heaps in which no form of disjunction exists (cf. Lemma 6).
 
6
Heap Automata for Reasoning about Robustness of Symbolic Heaps.
 
8
Two states \((s_1,h_1), (s_2,h_2)\) are isomorphic iff \( dom (s_1) = dom (s_2)\) and there exists a bijective function \(g : dom (h_1) \rightarrow dom (h_2)\) such that for all \(x \in dom (s_1)\) and all \(\ell \in dom (h_1)\), we have \(g(s_1(x)) = s_2(x)\) and \(g(h_1(\ell )) = h_2(g(\ell ))\), where g is lifted to tuples by componentwise application.
 
Literatur
1.
Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 411–425. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54830-7_​27CrossRefMATH
2.
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). doi:10.​1007/​978-3-540-73368-3_​22CrossRef
3.
4.
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006). doi:10.​1007/​11804192_​6CrossRef
5.
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_​5CrossRef
6.
Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​15CrossRef
7.
Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.: Permission accounting in separation logic. In: ACM SIGPLAN Notices, vol. 40, pp. 259–270. ACM (2005)
8.
Botincan, M., Distefano, D., Dodds, M., Grigore, R., Naudziuniene, D., Parkinson, M.J.: coreStar: the core of jStar. BOOGIE 2011, 65–77 (2011)
9.
10.
Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 131–146. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22438-6_​12CrossRefMATH
11.
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. ACM (2014)
12.
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, Heidelberg (2014). doi:10.​1007/​978-3-319-10936-7_​5CrossRef
13.
Brotherston, J., Gorogiannis, N., Kanovich, M.I., Rowe, R.: Model checking for symbolic-heap separation logic with inductive predicates. In: POPL 2016, pp. 84–96. ACM (2016)
14.
15.
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_​33CrossRef
16.
Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009, pp. 289–300. ACM (2009)
17.
Chin, W., 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)CrossRef
18.
Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, vol. 138. Cambridge University Press, Cambridge (2012)CrossRef
19.
Dodds, M.: From separation logic to hyperedge replacement and back. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 484–486. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-87405-8_​40CrossRef
20.
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_​29CrossRef
21.
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, Heidelberg (2014). doi:10.​1007/​978-3-319-12736-1_​17CrossRef
22.
Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI 2007, pp. 266–277. ACM (2007)
23.
Habermehl, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.: Forest automata for verification of heap manipulation. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 424–440. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​34CrossRefMATH
24.
Habermehl, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.: Forest automata for verification of heap manipulation. Formal Methods Syst. Des. 41(1), 83–106 (2012)CrossRef
25.
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRef
26.
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_​2CrossRef
27.
Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding entailments in inductive separation logic with tree automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 201–218. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-11936-6_​15CrossRef
28.
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-20398-5_​4CrossRef
29.
30.
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, Heidelberg (2014). doi:10.​1007/​978-3-319-08867-9_​4CrossRef
31.
Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: THOR: a tool for reasoning about shape and arithmetic. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 428–432. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-70545-1_​41CrossRef
32.
33.
Nguyen, H.H., Kuncak, V., Chin, W.-N.: Runtime checking for separation logic. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 203–217. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-78163-9_​19CrossRef
34.
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). doi:10.​1007/​3-540-44802-0_​1CrossRef
35.
O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)MathSciNetCrossRef
36.
37.
Qiu, X., Garg, P., Ştefănescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI 2013, pp. 231–242. ACM (2013)
38.
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE (2002)
39.
Zanardini, D., Genaim, S.: Inference of field-sensitive reachability and cyclicity. ACM Trans. Comput. Log. 15(4), 33:1–33:41 (2014)MathSciNetCrossRef
Metadaten
Titel
Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
verfasst von
Christina Jansen
Jens Katelaan
Christoph Matheja
Thomas Noll
Florian Zuleger
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
Buch
Programming Languages and Systems

Print ISBN: 978-3-662-54433-4

Electronic ISBN: 978-3-662-54434-1

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-662-54434-1_23