Implementation-level verification of algorithms with KeY

@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}
}