KIT | KIT-Bibliothek | Impressum | Datenschutz

Implementation-level Verification of Algorithms with KeY

Bruns, Daniel; Mostowski, Wojciech; Ulbrich, Mattias

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

Open Access Logo


Postprint §
DOI: 10.5445/IR/1000050296
Veröffentlicht am 31.01.2018
Originalveröffentlichung
DOI: 10.1007/s10009-013-0293-y
Scopus
Zitationen: 8
Web of Science
Zitationen: 3
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Zeitschriftenaufsatz
Publikationsjahr 2015
Sprache Englisch
Identifikator ISSN: 1433-2779, 1433-2787
urn:nbn:de:swb:90-502962
KITopen-ID: 1000050296
HGF-Programm 46.12.03 (POF III, LK 01)
Data Security
Erschienen in International journal on software tools for technology transfer
Band 17
Heft 6
Seiten 729 - 744
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
Schlagwörter formal verification, benchmark, Java Modeling Language, theorem prover
Nachgewiesen in Scopus
Web of Science
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page