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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Exploring an Interface Model for CKA Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

A Program Construction and Verification Tool for Separation Logic

verfasst von : Brijesh Dongol, Victor B. F. Gomes, Georg Struth

Erschienen in: Mathematics of Program Construction

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

An algebraic approach to the design of program construction and verification tools is applied to separation logic. The control-flow level is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data domain is captured by concrete store-heap models. These are linked to the separation algebra by soundness proofs. Verification conditions and transformation or refinement laws are derived by equational reasoning within the predicate transformer quantale. This separation of concerns makes an implementation in the Isabelle/HOL proof assistant simple and highly automatic. The resulting tool is itself correct by construction; it is explained on three simple examples.

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 Polynomial Functors Constrained by Regular Expressions
Nächstes Kapitel Calculating Certified Compilers for Non-deterministic Languages
Fußnoten
Literatur
1.
Armstrong, A., Gomes, V.B.F., Struth, G.: Algebraic principles for rely-guarantee style concurrency verification tools. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 78–93. Springer, Heidelberg (2014) CrossRef
2.
Armstrong, A., Gomes, V.B.F., Struth, G.: Lightweight program construction and verification tools in Isabelle/HOL. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 5–19. Springer, Heidelberg (2014) CrossRef
3.
Back, R.-J., von Wright, J.: Refinement Calculus. Springer, Berlin (1999) MATH
4.
Bergelson, V., Blass, A., Hindman, N.: Partition theorems for spaces of variable words. Proc. London Math. Soc. 68(3), 449–476 (1994)MathSciNetCrossRefMATH
5.
Berstel, J., Reutenauer, C.: Les séries rationnelles et leurs langagues. Masson (1984)
6.
Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 259–270. ACM (2005)
7.
Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS 2007, pp. 366–378. IEEE Computer Society (2007)
8.
Chlipala, A., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: Hutton, G., Tolmach, A.P. (eds.) ICFP 2009, pp. 79–90. ACM (2009)
9.
10.
Dang, H.-H., Möller, B.: Transitive separation logic. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 1–16. Springer, Heidelberg (2012) CrossRef
11.
Dang, H.-H., Möller, B.: Concurrency and local reasoning under reverse interchange. Sci. Comput. Program. 85, 204–223 (2014)CrossRef
12.
Day, B.: On closed categories of functors. In: MacLane, S., et al. (eds.) Reports of the Midwest Category Seminar IV. Lecture Notes in Mathematics, vol. 137, pp. 1–38. Springer, Heidelberg (1970) CrossRef
13.
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 287–300. ACM (2013)
14.
Distefano, D., Parkinson, M.J.: jstar: towards practical verification for Java. In: Harris, G.E. (ed.) OOPSLA 2008, pp. 213–226. ACM (2008)
15.
Dongol, B., Hayes, I.J., Struth, G.: Convolution, separation and concurrency. CoRR, abs/1312.1225 (2014)
16.
Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata, 1st edn. Springer, Heidelberg (2009) CrossRefMATH
17.
Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 215–237. Springer, Heidelberg (2013) CrossRef
18.
Gardiner, P.H.B., Martin, C.E., de Moor, O.: An algebraic construction of predicate transformers. Sci. Comput. Program. 22(1–2), 21–44 (1994)MathSciNetCrossRefMATH
19.
Guttmann, W., Struth, G., Weber, T.: Automating algebraic methods in Isabelle. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 617–632. Springer, Heidelberg (2011) CrossRef
20.
Hoare, C.A.R., Hussain, A., Möller, B., O’Hearn, P.W., Petersen, R.L., Struth, G.: On locality and the exchange law for concurrent processes. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 250–264. Springer, Heidelberg (2011) CrossRef
21.
Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent kleene algebra and its foundations. J. Log. Algebr. Program. 80(6), 266–296 (2011)MathSciNetCrossRefMATH
22.
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5(4), 596–619 (1983)CrossRefMATH
23.
Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 332–337. Springer, Heidelberg (2012) CrossRef
24.
25.
26.
27.
Morgan, C.: Programming from Specifications. Prentice-Hall, New York (1998)MATH
28.
Naumann, D.A.: Beyond fun: order and membership in polytypic imperative programming. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 286–314. Springer, Heidelberg (1998) CrossRef
29.
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) MATH
30.
31.
32.
O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001) CrossRef
33.
34.
Preoteasa, V.: Algebra of monotonic boolean transformers. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 140–155. Springer, Heidelberg (2011) CrossRef
35.
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)
36.
Smans, J., Jacobs, B., Piessens, F.: VeriFast for Java: a tutorial. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. LNCS, vol. 7850, pp. 407–442. Springer, Heidelberg (2013)
37.
Tuerk, T.: A Separation Logic Framework for HOL. Ph.D. thesis, Computer Laboratory, University of Cambridge (2011)
38.
V. Vafeiadis. Modular Fine-Grained Concurrency Verificaiton. PhD thesis, Computer Laboratory, University of Cambridge, 2007
39.
van Staden, S.: Constructing the Views Framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 62–83. Springer, Heidelberg (2015)
40.
Weber, T.: Towards Mechanized Program Verification with Separation Logic. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 250–264. Springer, Heidelberg (2004) CrossRefMATH
41.
Yang, H., O’Hearn, P.W.: A Semantic Basis for Local Reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002) CrossRef
Metadaten
Titel
A Program Construction and Verification Tool for Separation Logic
verfasst von
Brijesh Dongol
Victor B. F. Gomes
Georg Struth
Copyright-Jahr
2015
Verlag
Springer International Publishing
Buch
Mathematics of Program Construction

Print ISBN: 978-3-319-19796-8

Electronic ISBN: 978-3-319-19797-5

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-19797-5_7

Premium Partner

    Bildnachweise