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
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling
Erschienen in: Software and Systems Modeling 4/2016

25.12.2014 | Theme Section Paper

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

verfasst von: Stijn de Gouw, Frank de Boer, Wolfgang Ahrendt, Richard Bubel

Erschienen in: Software and Systems Modeling | Ausgabe 4/2016

Einloggen

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

search-config
loading …

Abstract

We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.
Vorheriger Artikel The Unit-B method: refinement guided by progress concerns
Nächster Artikel Contract-based verification of discrete-time multi-rate Simulink models

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 "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

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
Fußnoten
1
The benefit of delaying substitutions in the context of symbolic execution is illustrated in Sect. 6.
 
2
To see why the shifting inward of \({\{u\mathrel {:=}\,{\mathsf {new}\,}\}}\) is necessary, consider the case \({\{u\mathrel {:=}\,{\mathsf {new}\,}\}} (u.x=0)\). Neither side of the equality denotes the new object (at the top level), but the new object occurs in a sub-expression (namely \(u.x\)). With shifting, \({\{u\mathrel {:=}\,{\mathsf {new}\,}\}} (u.x=0)\) results in \((0=0)\). Without shifting, the (incorrect) result is \(u.x=0\).
 
3
As a counterexample, the term \({\{u\mathrel {:=}\,{\mathsf {new}\,}\}}u\) cannot be simplified further.
 
Literatur
1.
Abadi, M., Leino, K.R.M.: A logic of object-oriented programs. In: Proceedings of 7th International Conference Theory and Practice of Software, volume 1214 of Lecture Notes in Computer Science, pp. 682–696. Springer, Berlin (1997)
2.
Ábrahám, E., de Boer, F.S., de Roever, W.P., Steffen, M.: A deductive proof system for multithreaded Java with exceptions. Fundam. Inform. 82(4), 391–463 (2008)MathSciNetMATH
3.
Ahrendt, W., de Boer, F.S., Grabe, I.: Abstract object creation in dynamic logic. In: FM, pp. 612–627 (2009)
4.
Ahrendt, W., Mostowski, W., Paganelli, G.: Real-time Java API specifications for high coverage test generation. In: Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems. JTRES ’12, pp. 145–154. ACM, New York, USA (2012)
5.
America, P.: Designing an object-oriented programming language with behavioural subtyping. In: REX Workshop, pp. 60–90 (1990)
6.
America, P.: Formal techniques for parallel object-oriented languages. In: CONCUR, pp. 1–17 (1991)
7.
Apt, K.R.: Ten years of Hoare’s logic: a survey—part 1. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)CrossRefMATH
8.
Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of sequential and concurrent programs, 3rd edn. Texts in computer science. Springer, Berlin (2009). ISBN: 978-1-84882-744-8
9.
Apt, K.R., de Boer, F.S., Olderog, E.-R., de Gouw, S.: Verification of object-oriented programs: a transformational approach. J. Comput. Syst. Sci. 78(3), 823–852 (2012)MathSciNetCrossRefMATH
10.
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27–56 (2004)CrossRef
11.
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach, volume 4334 of Lecture Notes in Computer Science. Springer, Berlin (2007)
12.
Beckert, B., Klebanov, V., Schlager, S.: Dynamic logic. In: Beckert et al. [11], pp. 69–177
13.
Beckert, B., Platzer, A.: Dynamic logic with non-rigid functions. In: Furbach, U., Shankar, N. (eds.) IJCAR, volume 4130 of Lecture Notes in Computer Science, pp. 266–280. Springer, Berlin (2006)
14.
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: FMCO, pp. 115–137 (2005)
15.
Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory safety for systems-level code. In: CAV, pp. 178–183 (2011)
16.
Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filliâtre, J.-C., Grigore, R., Huisman, M., Klebanov, V., Marché, C., Monahan, R., Mostowski, W., Polikarpova, N., Scheben, C., Schellhorn, G., Tofan, B., Tschannen, J., Ulbrich, M.: The COST IC0701 verification competition 2011. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS, volume 7421 of Lecture Notes in Computer Science, pp. 3–21. Springer, Berlin (2011)
17.
Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. STTT 7(3), 212–232 (2005)CrossRef
18.
Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing ’74, pp. 308–312. Elsevier/North-Holland, Amsterdam (1974)
19.
Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI, San Diego, USA. USENIX Association (2008)
20.
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.) FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. vol. 2245, pp. 108–119, Springer, Berlin, Heidelberg (2001)
21.
Darvas, Á., Mehta, F., Rudich, A.: Efficient well-definedness checking. In: IJCAR, pp. 100–115 (2008)
22.
de Boer, F.S.: A WP-Calculus for OO. In: Thomas, W. (eds.) FoSSaCS, volume 1578 of Lecture Notes in Computer Science, pp. 135–149. Springer, Berlin (1999)
23.
de Gouw, S., de Boer, F.S., Ahrendt, W., Bubel, R.: Weak arithmetic completeness of object-oriented first-order assertion networks. In: SOFSEM, pp. 207–219 (2013)
24.
De Halleux, J., Tillmann, N.: Parameterized unit testing with Pex. In: Proceedings of 2nd International Conference on Tests and Proofs, LNCS, pp. 171–181. Springer, Berlin (2008)
25.
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)MATH
26.
Distefano, D., Parkinson, M.J.: jStar: Towards practical verification for Java. In: OOPSLA, pp. 213–226 (2008)
27.
Engel, C., Hähnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP, volume 4454 of Lecture Notes in Computer Science, pp. 169–188. Springer, Berlin (2007)
28.
Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: CAV, pp. 173–177 (2007)
29.
Galeotti, J., Rosner, N., Lopez Pombo, C., Frias, M.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Softw. Eng. 39(9), 1283–1307 (2013)CrossRef
30.
Giese, M.: First-order logic. In: Beckert et al. [11], pp. 21–68
31.
Harel, D.: Arithmetical completeness in logics of programs. In: ICALP, pp. 268–288 (1978)
32.
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). 583CrossRefMATH
33.
Huizing, K., Kuiper, R.: Verification of object-oriented programs using class invariants. Fundam. Approach. Softw. Eng. 1783, 208–221 (2000)CrossRef
34.
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Proceedings of the Third international conference on NASA Formal Methods, NFM’11, pp. 41–55, Springer, Berlin, Heidelberg (2011)
35.
Kassios, I.T., Müller, P., Schwerhoff, M.: Comparing verification condition generation with symbolic execution: an experience report. In: Proceedings of the 4th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE’12, pp. 196–208, Springer, Berlin, Heidelberg (2012)
36.
37.
Klebanov, V., Müller, P., Shankar, N., Leavens, G.T., Wüstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Weiß, B.: The 1st verified software competition: experience report. In: Proceedings of the 17th International Conference on Formal Methods. FM’11, pp. 154–168. Springer, Berlin, Heidelberg (2011)
38.
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. Trans. Program. Lang. Syst. 28(4), 619–695 (2006)CrossRef
39.
Leavens, G.T., Kiniry, J.R., Poll, E.: A JML tutorial: Modular specification and verification of functional behavior for Java. In: CAV, p. 37 (2007)
40.
Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B., Leavens, G.T., Ruby, C.: JML: Notations and tools supporting detailed design in Java. In: In OOPSLA 2000 Companion, pp. 105–106. ACM (2000)
41.
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR (Dakar), volume 6355 of Lecture Notes in Computer Science, pp. 348–370. Springer, Berlin (2010)
42.
Leino, K.R.M., Müller, P., Smans, J.: Foundations of security analysis and design V. In: Chapter Verification of Concurrent Programs with Chalice, pp. 195–222. Springer, Berlin, Heidelberg (2009)
43.
Leino, K.R.M., Müller, P., Smans, J.: Deadlock-free channels and locks. In: Proceedings of the 19th European Conference on Programming Languages and Systems. ESOP’10, pp. 407–426. Springer, Berlin, Heidelberg (2010)
44.
Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994)CrossRef
45.
Mostowski, W.: Formalisation and verification of Java card security properties in dynamic logic. In: Cerioli, M. (ed.) Proceedings of Fundamental Approaches to Software Engineering (FASE), Edinburgh, volume 3442 of Lecture Notes in Computer Science, pp. 357–371. Springer, Berlin (2005)
46.
Mostowski, W.: Fully verified Java Card API reference implementation. In: Beckert, B. (ed), VERIFY (2007)
47.
Object Modeling Group: Object Constraint Language Specification, Version 2.0, June (2005)
48.
49.
Rümmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A, (eds.) LPAR, volume 4246 of Lecture Notes in Computer Science, pp. 422–436. Springer, Berlin (2006)
50.
51.
Tucker, J., Zucker, J.: Program Correctness over Abstract Data Types, With Error-State Semantics. Elsevier Science, Amsterdam (1988)MATH
52.
van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS, volume 2031 of Lecture Notes in Computer Science, pp. 299–312. Springer, Berlin (2001)
53.
Wittgenstein, L.: Tractatus logico-Philosophicus. London: Routledge, 1981 (1922)
Metadaten
Titel
Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic
verfasst von
Stijn de Gouw
Frank de Boer
Wolfgang Ahrendt
Richard Bubel
Publikationsdatum
25.12.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 4/2016
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-014-0446-9

Weitere Artikel der Ausgabe 4/2016

Software and Systems Modeling 4/2016 Zur Ausgabe

Theme Section Paper

An overview of model checking practices on verification of PLC software

Theme Section Paper

Model-checking software library API usage rules

Guest Editorial

Theme issue on Integrated Formal Methods

Theme Section Paper

Automated anonymity verification of the ThreeBallot and VAV voting systems

Regular Paper

Supporting different process views through a Shared Process Model

Theme Section Paper

The Unit-B method: refinement guided by progress concerns

Premium Partner

    Bildnachweise