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 | VerifyThis 2012

Let’s verify this with Why3

verfasst von: François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich

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 present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.
Vorheriger Artikel SPARK 2014 and GNATprove
Nächster Artikel Implementation-level verification of algorithms with KeY

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
1
Notice that the non-ghost fields of https://static-content.springer.com/image/art%3A10.1007%2Fs10009-014-0314-5/MediaObjects/10009_2014_314_IEq17_HTML.gif can still be used in regular, non-ghost code, which would not be the case were https://static-content.springer.com/image/art%3A10.1007%2Fs10009-014-0314-5/MediaObjects/10009_2014_314_IEq18_HTML.gif declared as a https://static-content.springer.com/image/art%3A10.1007%2Fs10009-014-0314-5/MediaObjects/10009_2014_314_IEq19_HTML.gif type.
 
2
Another purpose of transformations is to eliminate and encode various high-level features of Why3 language, such as pattern matching or type polymorphism, to make proof obligations acceptable for a range of external provers. These transformations are invoked by a driver for a particular prover and do not need to be applied explicitly by the user.
 
3
Calling a method on an object before it is fully constructed is indeed not recommended [18].
 
4
That came to our mind during the competition.
 
Literatur
1.
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd international conference on Computer aided verification, CAV’11, pp. 171–177. Heidelberg, Berlin (2011)
2.
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) 19th International Conference on Computer Aided Verification, vol 4590 of Lecture Notes in Computer Science, pp. 298–302. Springer, Berlin (2007)
3.
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer-Verlag, Berlin (2004)MATHCrossRef
4.
5.
Bobot, F., Filliâtre, J.-C., Marché, C., Melquiond, G., Paskevich, A.: Preserving user proofs across specification changes. In: Cohen, E., Rybalchenko, A. (eds.) Verified software: theories, tools, experiments (5th International Conference VSTTE), vol 8164 of Lecture Notes in Computer Science, pp. 191–201. Springer, Atherton (2013)
6.
7.
Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie (ed.) First International Workshop on Intermediate Verification Languages, pp. 53–64. Wrocław, Poland (2011)
8.
de Moura, L., Bjørner, N.: Z3, an efficient SMT solver. In: TACAS, vol 4963 of Lecture Notes in Computer Science, pp. 337–340. Springer, Berlin (2008)
9.
Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Proceedings of the 22nd European Symposium on Programming, vol 7792 of Lecture Notes in Computer Science, pp. 125–128. Springer, Berlin (2013)
10.
11.
12.
Leino, K.R.M., Moskal, M.: VACID-0: Verification of ample correctness of invariants of data-structures. In: Proceedings of Tools and Experiments Workshop at VSTTE (2010)
13.
14.
15.
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed). 11th International Conference on Automated Deduction, vol 607 of Lecture Notes in Computer Science, pp. 748–752. Springer, Saratoga Springs (1992)
16.
Riazanov, A., Voronkov, A.: Vampire. In: Ganzinger, H. (ed.) 16th International Conference on Automated Deduction, vol 1632 of Lecture Notes in Artificial Intelligence, pp. 292–296. Springer, Trento (1999)
17.
Schulz, S.: System description: E 0.81. In: Basin, D.A., Rusinowitch, M. (eds) Second International Joint Conference on Automated Reasoning, vol 3097 of Lecture Notes in Computer Science, pp. 223–228. Springer, Berlin (2004)
18.
Summers, A.J., Mueller, P.: Freedom before commitment: a lightweight type system for object initialisation. In: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications, OOPSLA ’11, pp. 1013–1032. ACM, New York (2011)
19.
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) 22nd International Conference on Automated Deduction, vol 5663 of Lecture Notes in Computer Science, pp 140–145. Springer, Berlin (2009)
Metadaten
Titel
Let’s verify this with Why3
verfasst von
François Bobot
Jean-Christophe Filliâtre
Claude Marché
Andrei Paskevich
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-014-0314-5

Weitere Artikel der Ausgabe 6/2015

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

VerifyThis 2012

SPARK 2014 and GNATprove

VerifyThis 2012

Implementation-level verification of algorithms with KeY

VerifyThis 2012

KIV: overview and VerifyThis competition

Introduction

VerifyThis 2012

VerifyThis 2012

Witnessing the elimination of magic wands

VerifyThis 2012

AutoProof meets some verification challenges

Premium Partner

    Bildnachweise