Implementation-level verification of algorithms with KeY

Daniel Bruns; Wojciech Mostowski; Mattias Ulbrich

doi:10.1007/s10009-013-0293-y

Implementation-level verification of algorithms with KeY

Daniel Bruns, Wojciech Mostowski, Mattias Ulbrich

Research output: Contribution to journal › Article › Academic › peer-review

9 Citations (Scopus)

1 Downloads (Pure)

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.

Original language	English
Pages (from-to)	729-744
Number of pages	16
Journal	International journal on software tools for technology transfer
Volume	17
Issue number	6
DOIs	https://doi.org/10.1007/s10009-013-0293-y
Publication status	Published - 17 Nov 2013

Keywords

Theorem prover
Formal verification
Benchmark
Java modeling language

Access to Document

10.1007/s10009-013-0293-y

Cite this

@article{7efd3a4a901d43f6919b9489989c676f,

title = "Implementation-level verification of algorithms with KeY",

abstract = "We give an account on the authors{\textquoteright} 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.",

keywords = "Theorem prover, Formal verification, Benchmark, Java modeling language",

author = "Daniel Bruns and Wojciech Mostowski and Mattias Ulbrich",

year = "2013",

month = nov,

day = "17",

doi = "10.1007/s10009-013-0293-y",

language = "English",

volume = "17",

pages = "729--744",

journal = "International journal on software tools for technology transfer",

issn = "1433-2779",

publisher = "Springer",

number = "6",

}

TY - JOUR

T1 - Implementation-level verification of algorithms with KeY

AU - Bruns, Daniel

AU - Mostowski, Wojciech

AU - Ulbrich, Mattias

PY - 2013/11/17

Y1 - 2013/11/17

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

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

KW - Theorem prover

KW - Formal verification

KW - Benchmark

KW - Java modeling language

U2 - 10.1007/s10009-013-0293-y

DO - 10.1007/s10009-013-0293-y

M3 - Article

SN - 1433-2779

VL - 17

SP - 729

EP - 744

JO - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

IS - 6

ER -

Implementation-level verification of algorithms with KeY

Abstract

Keywords

Access to Document

Fingerprint

Cite this