Skip to main content
Erschienen in: International Journal on Software Tools for Technology Transfer 6/2015

01.11.2015 | VerifyThis 2012

Implementation-level verification of algorithms with KeY

verfasst von: Daniel Bruns, Wojciech Mostowski, Mattias Ulbrich

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2015

Einloggen

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

search-config
loading …

Abstract

We give an account on the authors’ experience and results from the software verification competition held at the Formal Methods 2012 conference. Competitions like this are meant to provide a benchmark for verification systems. It consisted of three algorithms which the authors have implemented in Java, specified with the Java Modeling Language, and verified using the KeY system. Building on our solutions, we argue that verification systems which target implementations in real-world programming languages better have powerful abstraction capabilities. Regarding the KeY tool, we explain features which, driven by the competition, have been freshly implemented to accommodate for these demands.

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!

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!

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!

Fußnoten
1
For an empirical analysis of user experience with KeY, see [2].
 
2
In this case, we also need to prove that no runtime exceptions, such as NullPointer Exception or IndexOutOfBounds Exception, are raised.
 
3
For all proofs, KeY was running on standard desktop computers in single-processor mode.
 
4
This is in fact essential to this algorithm being parallelisable.
 
5
Currently, we only support single return statements for the body, i.e., definitions can be only given with direct formulae, rather than proper Java programs that involve, e.g., loops or similar constructs.
 
6
This would not have been the case if we had used a ghost field to track the exact size of the tree by precisely adding sub-tree sizes.
 
Literatur
1.
Zurück zum Zitat Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), International Workshop, 2004, Revised Selected Papers. LNCS, vol. 3362, pp. 49–69. Springer (2005) Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), International Workshop, 2004, Revised Selected Papers. LNCS, vol. 3362, pp. 49–69. Springer (2005)
2.
Zurück zum Zitat Beckert, B., Grebing, S.: Evaluating the usability of interactive verification systems. In: Klebanov, V., Beckert, B., Biere, A., Sutcliffe, G. (eds.) 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE) 2012, CEUR Workshop Proceedings, vol. 873 (2012) Beckert, B., Grebing, S.: Evaluating the usability of interactive verification systems. In: Klebanov, V., Beckert, B., Biere, A., Sutcliffe, G. (eds.) 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE) 2012, CEUR Workshop Proceedings, vol. 873 (2012)
3.
Zurück zum Zitat Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer (2007) Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer (2007)
4.
Zurück zum Zitat Blelloch, G.E.: Prefix sums and their applications. Tech. Rep. CMU-CS-90-190, School of Computer Science, Carnegie Mellon University (1990) Blelloch, G.E.: Prefix sums and their applications. Tech. Rep. CMU-CS-90-190, School of Computer Science, Carnegie Mellon University (1990)
5.
Zurück zum Zitat 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.) Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011). LNCS, vol. 7421, pp. 3–21. Springer (2012) 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.) Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011). LNCS, vol. 7421, pp. 3–21. Springer (2012)
6.
Zurück zum Zitat Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03). ENTCS, vol. 80, pp. 73–89. Elsevier (2003) Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03). ENTCS, vol. 80, pp. 73–89. Elsevier (2003)
7.
Zurück zum Zitat Cheon, Y., Leavens, G.T., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Exp. 35(6), 583–599 (2005)CrossRef Cheon, Y., Leavens, G.T., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Exp. 35(6), 583–599 (2005)CrossRef
8.
Zurück zum Zitat De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRef De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRef
9.
Zurück zum Zitat Filliâtre, J.C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) 19th International Conference on Computer Aided Verification. LNCS, vol. 4590. Springer (2007) Filliâtre, J.C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) 19th International Conference on Computer Aided Verification. LNCS, vol. 4590. Springer (2007)
10.
Zurück zum Zitat Filliâtre, J.C., Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: Beckert, B., Biere, A., Klebanov, V., Sutcliffe, G. (eds.) 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE) 2012, CEUR Workshop Proceedings, vol. 873 (2012) Filliâtre, J.C., Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: Beckert, B., Biere, A., Klebanov, V., Sutcliffe, G. (eds.) 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE) 2012, CEUR Workshop Proceedings, vol. 873 (2012)
11.
Zurück zum Zitat Harel, D.: Dynamic logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic, pp. 497–604. D. Reidel Publishing Co., Dordrecht (1984)CrossRef Harel, D.: Dynamic logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic, pp. 497–604. D. Reidel Publishing Co., Dordrecht (1984)CrossRef
12.
Zurück zum Zitat 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.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods—Third International Symposium, 2011. LNCS, vol. 6617, pp. 41–55. Springer (2011) 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.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods—Third International Symposium, 2011. LNCS, vol. 6617, pp. 41–55. Springer (2011)
14.
Zurück zum Zitat Kassios, I.T., Müller, P., Schwerhoff, M.: Comparing verification condition generation with symbolic execution: an experience report. In: Joshi, R., Müller, P., Podelski, A. (eds.) Verified Software Theories Tools Experiments (VSTTE) 2012. LNCS, vol. 7152, pp. 196–208. Springer (2012) Kassios, I.T., Müller, P., Schwerhoff, M.: Comparing verification condition generation with symbolic execution: an experience report. In: Joshi, R., Müller, P., Podelski, A. (eds.) Verified Software Theories Tools Experiments (VSTTE) 2012. LNCS, vol. 7152, pp. 196–208. Springer (2012)
15.
Zurück zum Zitat 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: Butler, M., Schulte, W. (eds.) Proceedings, 17th International Symposium on Formal Methods (FM) 2011. LNCS, vol. 6664, pp. 154–168. Springer (2011) 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: Butler, M., Schulte, W. (eds.) Proceedings, 17th International Symposium on Formal Methods (FM) 2011. LNCS, vol. 6664, pp. 154–168. Springer (2011)
16.
Zurück zum Zitat Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT 31(3), 1–38 (2006)CrossRef Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT 31(3), 1–38 (2006)CrossRef
17.
Zurück zum Zitat Mostowski, W.: Formal reasoning about non-atomic Java Card methods in dynamic logic. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) Proceedings, Formal Methods (FM) 2006. LNCS, vol. 4085, pp. 444–459. Springer (2006) Mostowski, W.: Formal reasoning about non-atomic Java Card methods in dynamic logic. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) Proceedings, Formal Methods (FM) 2006. LNCS, vol. 4085, pp. 444–459. Springer (2006)
18.
Zurück zum Zitat Mostowski, W.: Fully verified Java Card API reference implementation. In: Beckert, B. (ed.) 4th International Verification Workshop, CEUR WS, vol. 259 (2007) Mostowski, W.: Fully verified Java Card API reference implementation. In: Beckert, B. (ed.) 4th International Verification Workshop, CEUR WS, vol. 259 (2007)
20.
Zurück zum Zitat Parkinson, M., Bierman, G.: Separation logic and abstraction. SIGPLAN Notes 40(1), 247–258 (2005) Parkinson, M., Bierman, G.: Separation logic and abstraction. SIGPLAN Notes 40(1), 247–258 (2005)
21.
Zurück zum Zitat Scheben, C., Schmitt, P.H.: Verification of information flow properties of Java programs without approximations. In: Formal Verification of Object-Oriented Software. LNCS, vol. 7421, pp. 232–249. Springer (2012) Scheben, C., Schmitt, P.H.: Verification of information flow properties of Java programs without approximations. In: Formal Verification of Object-Oriented Software. LNCS, vol. 7421, pp. 232–249. Springer (2012)
22.
Zurück zum Zitat Schmitt, P.H., Tonin, I.: Verifying the Mondex case study. In: Hinchey, M., Margaria, T. (eds.) Proceedings of the 5th IEEE International Conference on Software Engineeging and Formal Methods (SEFM), pp. 47–56. IEEE Press (2007) Schmitt, P.H., Tonin, I.: Verifying the Mondex case study. In: Hinchey, M., Margaria, T. (eds.) Proceedings of the 5th IEEE International Conference on Software Engineeging and Formal Methods (SEFM), pp. 47–56. IEEE Press (2007)
24.
Zurück zum Zitat Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley, Reading (2011) Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley, Reading (2011)
25.
Zurück zum Zitat Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004. LNCS, vol. 3116, pp. 491–505. Springer (2004) Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004. LNCS, vol. 3116, pp. 491–505. Springer (2004)
26.
Zurück zum Zitat Weiß, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (2011) Weiß, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (2011)
Metadaten
Titel
Implementation-level verification of algorithms with KeY
verfasst von
Daniel Bruns
Wojciech Mostowski
Mattias Ulbrich
Publikationsdatum
01.11.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 6/2015
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-013-0293-y

Weitere Artikel der Ausgabe 6/2015

International Journal on Software Tools for Technology Transfer 6/2015 Zur Ausgabe

Introduction

VerifyThis 2012

Premium Partner