KIT | KIT-Bibliothek | Impressum
Open Access Logo
DOI: 10.5445/IR/1000050296

Implementation-level Verification of Algorithms with KeY

Bruns, Daniel; Mostowski, Wojciech; Ulbrich, Mattias

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 are required to have powerful capabilities for abstraction. Regarding the KeY tool, we explain features which, driven by the competition, have been freshly implemented to accommodate for these demands.

Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Zeitschriftenaufsatz
Jahr 2015
Sprache Englisch
Identifikator ISSN: 1433-2779, 1433-2787
URN: urn:nbn:de:swb:90-502962
KITopen ID: 1000050296
HGF-Programm 46.12.03; LK 01
Erschienen in International journal on software tools for technology transfer
Band 17
Heft 6
Seiten 729 - 744
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
Schlagworte formal verification, benchmark, Java Modeling Language, theorem prover
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page