Implementation-level verification of algorithms with KeY

Zeitschriftenartikel

Autor(en):Daniel Bruns, Wojciech Mostowski und Mattias Ulbrich
Zeitschrift:International Journal on Software Tools for Technology Transfer (STTT)
Verleger:Springer
Nummer:6
Band:17
Jahr:2013
Seiten:729-744
DOI:10.1007/s10009-013-0293-y
Stichworte: Formal verification; Benchmark; Java Modeling Language; Theorem prover

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.

BibTeX

@ARTICLE{BrunsMostowskiUlbrich2013,
  author = {Daniel Bruns and Wojciech Mostowski and Mattias Ulbrich},
  title = {Implementation-level verification of algorithms with {\KeY}},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  year = {2013},
  month = nov,
  volume = {17},
  number = {6},
  pages = {729--744},
  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.},
  doi = {10.1007/s10009-013-0293-y},
  issn = {1433-2779},
  keywords = {Formal verification; Benchmark; Java Modeling Language; Theorem prover},
  language = {English},
  publisher = {Springer}
}