The KeY platform for verification and analysis of Java programs

Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, Mattias Ulbrich

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)
    50 Downloads (Pure)

    Abstract

    The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.
    Original languageEnglish
    Title of host publicationVerified Software: Theories, Tools and Experiments
    Subtitle of host publication6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers
    EditorsDimitra Giannakopoulou, Daniel Kroening
    Place of PublicationCham
    PublisherSpringer
    Pages55-71
    Number of pages17
    ISBN (Electronic)978-3-319-12154-3
    ISBN (Print)978-3-319-12153-6
    DOIs
    Publication statusPublished - 14 Oct 2014

    Publication series

    NameLecture Notes In Computer Science
    PublisherSpringer
    Volume8471
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Fingerprint

    Acoustic waves
    Testing
    Modeling languages
    Code generation
    Formal verification

    Keywords

    • Testing
    • System description
    • Theorem proving
    • Java
    • Visualization
    • Verification
    • Security

    Cite this

    Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., ... Ulbrich, M. (2014). The KeY platform for verification and analysis of Java programs. In D. Giannakopoulou, & D. Kroening (Eds.), Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers (pp. 55-71). (Lecture Notes In Computer Science; Vol. 8471). Cham: Springer. https://doi.org/10.1007/978-3-319-12154-3_4
    Ahrendt, Wolfgang ; Beckert, Bernhard ; Bruns, Daniel ; Bubel, Richard ; Gladisch, Christoph ; Grebing, Sarah ; Hähnle, Reiner ; Hentschel, Martin ; Herda, Mihai ; Klebanov, Vladimir ; Mostowski, Wojciech ; Scheben, Christoph ; Schmitt, Peter H. ; Ulbrich, Mattias. / The KeY platform for verification and analysis of Java programs. Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. editor / Dimitra Giannakopoulou ; Daniel Kroening. Cham : Springer, 2014. pp. 55-71 (Lecture Notes In Computer Science).
    @inproceedings{5f9412d3c2fd43d58d1f3a2077f2b6ec,
    title = "The KeY platform for verification and analysis of Java programs",
    abstract = "The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.",
    keywords = "Testing, System description, Theorem proving, Java, Visualization, Verification, Security",
    author = "Wolfgang Ahrendt and Bernhard Beckert and Daniel Bruns and Richard Bubel and Christoph Gladisch and Sarah Grebing and Reiner H{\"a}hnle and Martin Hentschel and Mihai Herda and Vladimir Klebanov and Wojciech Mostowski and Christoph Scheben and Schmitt, {Peter H.} and Mattias Ulbrich",
    note = "eemcs-eprint-25325",
    year = "2014",
    month = "10",
    day = "14",
    doi = "10.1007/978-3-319-12154-3_4",
    language = "English",
    isbn = "978-3-319-12153-6",
    series = "Lecture Notes In Computer Science",
    publisher = "Springer",
    pages = "55--71",
    editor = "Dimitra Giannakopoulou and Daniel Kroening",
    booktitle = "Verified Software: Theories, Tools and Experiments",

    }

    Ahrendt, W, Beckert, B, Bruns, D, Bubel, R, Gladisch, C, Grebing, S, Hähnle, R, Hentschel, M, Herda, M, Klebanov, V, Mostowski, W, Scheben, C, Schmitt, PH & Ulbrich, M 2014, The KeY platform for verification and analysis of Java programs. in D Giannakopoulou & D Kroening (eds), Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. Lecture Notes In Computer Science, vol. 8471, Springer, Cham, pp. 55-71. https://doi.org/10.1007/978-3-319-12154-3_4

    The KeY platform for verification and analysis of Java programs. / Ahrendt, Wolfgang; Beckert, Bernhard; Bruns, Daniel; Bubel, Richard; Gladisch, Christoph; Grebing, Sarah; Hähnle, Reiner; Hentschel, Martin; Herda, Mihai; Klebanov, Vladimir; Mostowski, Wojciech; Scheben, Christoph; Schmitt, Peter H.; Ulbrich, Mattias.

    Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. ed. / Dimitra Giannakopoulou; Daniel Kroening. Cham : Springer, 2014. p. 55-71 (Lecture Notes In Computer Science; Vol. 8471).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - The KeY platform for verification and analysis of Java programs

    AU - Ahrendt, Wolfgang

    AU - Beckert, Bernhard

    AU - Bruns, Daniel

    AU - Bubel, Richard

    AU - Gladisch, Christoph

    AU - Grebing, Sarah

    AU - Hähnle, Reiner

    AU - Hentschel, Martin

    AU - Herda, Mihai

    AU - Klebanov, Vladimir

    AU - Mostowski, Wojciech

    AU - Scheben, Christoph

    AU - Schmitt, Peter H.

    AU - Ulbrich, Mattias

    N1 - eemcs-eprint-25325

    PY - 2014/10/14

    Y1 - 2014/10/14

    N2 - The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.

    AB - The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.

    KW - Testing

    KW - System description

    KW - Theorem proving

    KW - Java

    KW - Visualization

    KW - Verification

    KW - Security

    U2 - 10.1007/978-3-319-12154-3_4

    DO - 10.1007/978-3-319-12154-3_4

    M3 - Conference contribution

    SN - 978-3-319-12153-6

    T3 - Lecture Notes In Computer Science

    SP - 55

    EP - 71

    BT - Verified Software: Theories, Tools and Experiments

    A2 - Giannakopoulou, Dimitra

    A2 - Kroening, Daniel

    PB - Springer

    CY - Cham

    ER -

    Ahrendt W, Beckert B, Bruns D, Bubel R, Gladisch C, Grebing S et al. The KeY platform for verification and analysis of Java programs. In Giannakopoulou D, Kroening D, editors, Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. Cham: Springer. 2014. p. 55-71. (Lecture Notes In Computer Science). https://doi.org/10.1007/978-3-319-12154-3_4