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

    Keywords

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

    Fingerprint Dive into the research topics of 'The KeY platform for verification and analysis of Java programs'. Together they form a unique fingerprint.

  • 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