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
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 6/2015

01.11.2015 | Introduction

VerifyThis 2012

A Program Verification Competition

verfasst von: Marieke Huisman, Vladimir Klebanov, Rosemary Monahan

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

VerifyThis 2012 was a 2-day verification competition that took place as part of the International Symposium on Formal Methods (FM 2012) on August 30–31, 2012, in Paris, France. It was the second installment in the VerifyThis series. After the competition, an open call solicited contributions related to the VerifyThis 2012 challenges and overall goals. As a result, seven papers were submitted and, after review and revision, included in this special issue. In this introduction to the special issue, we provide an overview of the VerifyThis competition series, an account of related activities in the area, and an overview of solutions submitted to the organizers both during and after the 2012 competition. We conclude with a summary of results and some remarks concerning future installments of VerifyThis.
Nächster Artikel Solving the VerifyThis 2012 challenges with VeriFast

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
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
2
In particular, because the author of the best challenge submission was participating in the competition.
 
8
Available as part of the original challenge http://​fm2012.​verifythis.​org and in Appendix 6.
 
9
The original challenge description contained an illustrating excerpt from a slide deck on prefix sums.
 
10
AutoProof has been significantly improved since its 2013 version used here.
 
11
This specification uses a loop contract. If the tool supported contracts for arbitrary code blocks, then the modification after the loop could be included and a simpler solution as proposed by Tuerk would have been possible.
 
Literatur
1.
Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., Hähnle, R., Hentschel, M., Klebanov, V., Mostowski, W., Scheben, C., Schmitt, P.H., Ulbrich, M.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D., Polgreen, E., Shankar, N., (eds) Proceedings, 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), Vienna, July 2014, LNCS. Springer (2014)
2.
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) International Conference on Formal Verification of Object-Oriented Systems (FoVeOOS 2011), LNCS. Springer (2012)
3.
Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Let’s verify this with Why3. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)
4.
Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Formal Methods of LNCS, vol. 8442, pp. 127–131. Springer (2014)
5.
Blom, S., Huisman, M.: Witnessing the elimination of magic wands. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)
6.
Beyer, Dirk, Huisman, Marieke, Klebanov, Vladimir, Monahan, Rosemary: Evaluating software verification systems: benchmarks and competitions (Dagstuhl Reports 14171). Dagstuhl Rep 4(4), 1–19 (2014)
7.
Guy, E.: Blelloch. Prefix sums and their applications. In: Reif, John H. (ed.) Synthesis of parallel algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1993)
8.
Broy, M., Merz, S., Spies, K.: (ed) Formal systems specification. In: The RPC-Memory Specification Case Study of LNCS, vol. 1169. Springer (1996)
9.
Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)
10.
Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., MichałMoskal, S., Thomas, S., Wolfram, T.S.: VCC: a practical system for verifying concurrent C. In: Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’09, pp. 23–42. Springer-Verlag (2009)
11.
Chong, N.: Scalable verification techniques for data-parallel programs. PhD thesis, Imperial College London (2014)
12.
Cok, D.R., Kiniry, J.R.: Esc/java2: Uniting ESC/Java and JML. In: Proceedings of the 2004 International Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS’04, pp. 108–128. Springer-Verlag (2005)
13.
Craigen, D.: Strengths and weaknesses of program verification systems. In: Proceedings of the 1st European Software Engineering Conference on ESEC ’87, pp. 396–404. Springer-Verlag (1987)
14.
Dross, C., Efstathopoulos, P., Lesens, D., Mentré, D., Moy, Y.: Rail, space, security: Three case studies for SPARK 2014. In: 7th Europen Congress on Embedded Real Time Software and Systems (ERTS\(^{2}\) 2014) (2014)
15.
Ernst, G., Pfähler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)
16.
Filliâtre J.-C., Paskevich, A.: Why3: where programs meet provers. In: Proceedings of the 22nd European Conference on Programming Languages and Systems, ESOP’13, pp. 125–128. Springer-Verlag (2013)
17.
Filliâtre, J.-C, Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: Klebanov, V., Biere, A., Beckert, B., Sutcliffe, G. (eds) Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012) (2012)
18.
Huisman, M., Klebanov, V., Monahan, R.: On the organisation of program verification competitions. In: Vladimir, K., Bernhard, B., Biere A., Sutcliffe, G. (eds) Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE), Manchester, UK, June 30, 2012, of CEUR Workshop Proceedings. vol. 873, CEUR-WS.org (2012)
19.
Hoang, D., Moy, Y., Wallenburg, A., Chapman, R.: SPARK 2014 and GNATprove. A competition report from builders of an industrial-strength verifying compiler. Int. J. Softw. Tools Technol. (Transfer, in this issue) (2015)
20.
21.
Jacobs, B., Smans, J., Piessens, F.: Solving the VerifyThis: challenges with VeriFast, p. 2015. J. Softw. Tools Technol. Transfer, (in this issue, Int) (2012)
22.
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: Michael, B., Wolfram, S., (eds) Proceedings, 17th International Symposium on Formal Methods (FM) of LNCS, vol. 6664. Springer (2011)
23.
Kärkkäinen, J., Sanders, P.: Simple linear work suffix array construction. In: Proceedings of the 30th International Conference on Automata, languages and programming, ICALP’03, pp. 943–955, Berlin, Heidelberg, Springer-Verlag (2003)
24.
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’10, pp. 348–370. Springer-Verlag (2010)
25.
Lewerentz, C., Lindner, T.: Case study “production cell”: a comparative study in formal specification and verification. In: Manfred, B., Stefan, J., (eds) KORSO: Methods, Languages, and Tools for the Construction of Correct Software of LNCS, vol. 1009, pp. 388–416. Springer (1995)
26.
Leavens, Gary T., Leino, K.Rustan M., Müller, Peter: Specification and verification challenges for sequential object-oriented programs. Form. Asp. Comput. 19, 159–189 (2007)MATHCrossRef
27.
Leino, K.R.M., Moskal, M.: VACID-0: verification of ample correctness of invariants of data-structures, edn 0. In: Proceedings of Tools and Experiments Workshop at VSTTE (2010)
28.
Liu, Y., Sun, J., Dong, J.S.: Developing model checkers using PAT. In: Proceedings of the 8th International Conference on Automated Technology for Verification and Analysis, ATVA’10, pp. 371–377. Springer-Verlag (2010)
29.
Philippaerts, P., Mühlberg, J.Tobias, Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with verifast. Sci. Comput. Program. 82, 77–97 (2014)CrossRef
30.
Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Wolfgang, B., Peter H.S. (eds) Automated deduction—a basis for applications of applied logic series, vol. 9 , pp. 13–39. Springer, Netherlands (1998)
31.
Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley, USA (2011)
32.
Tschannen, J., Furia, C.A., Martin, N.: AutoProof meets some verification challenges. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)
33.
Tuerk, T.: Local reasoning about while-loops. In: Müller, P., Naumann, D., Yang, H. (eds) Proceedings VS-Theory Workshop of VSTTE, pp. 29–39 (2010)
34.
Woodcock, J.: First steps in the verified software grand challenge. Computer 39(10), 57–64 (2006)CrossRef
35.
Weide, B.W., Sitaraman, M., Harton, H.K., Adcock, B.M., Bucci, P., Bronish, D., Heym, W.D., Kirschenbaum, J., Frazier, D.: Incremental benchmarks for software verification tools and techniques. In: Shankar, N., Woodcock, J. (eds) Proceedings verified software: theories, tools, experiments (VSTTE) of LNCS, vol. 5295, pp. 84–98. Springer (2008)
Metadaten
Titel
VerifyThis 2012
A Program Verification Competition
verfasst von
Marieke Huisman
Vladimir Klebanov
Rosemary Monahan
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-015-0396-8

Weitere Artikel der Ausgabe 6/2015

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

VerifyThis 2012

KIV: overview and VerifyThis competition

VerifyThis 2012

Solving the VerifyThis 2012 challenges with VeriFast

VerifyThis 2012

Witnessing the elimination of magic wands

VerifyThis 2012

AutoProof meets some verification challenges

VerifyThis 2012

Implementation-level verification of algorithms with KeY

VerifyThis 2012

Let’s verify this with Why3

Premium Partner

    Bildnachweise