Implementation-level verification of algorithms with KeY

Daniel Bruns, Wojciech Mostowski, Mattias Ulbrich

    Research output: Contribution to journalArticleAcademicpeer-review

    8 Citations (Scopus)

    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 languageEnglish
    Pages (from-to)729-744
    Number of pages16
    JournalInternational journal on software tools for technology transfer
    Volume17
    Issue number6
    DOIs
    Publication statusPublished - 17 Nov 2013

    Keywords

    • Theorem prover
    • Formal verification
    • Benchmark
    • Java modeling language

    Fingerprint Dive into the research topics of 'Implementation-level verification of algorithms with KeY'. Together they form a unique fingerprint.

    Cite this