Reasoning About JML: Differences Between KeY and OpenJML

Jan Boerman, Marieke Huisman, Sebastiaan Jozef Christiaan Joosten

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

    1 Citation (Scopus)
    111 Downloads (Pure)


    To increase the impact and capabilities of formal verification, it should be possible to apply different verification techniques on the same specification. However, this can only be achieved if verification tools agree on the syntax and underlying semantics of the specification language and unfortunately, in practice, this is often not the case.
    In this paper, we concentrate on one particular example, namely Java programs annotated with JML, and we present a case study in understanding differences in the treatment of these specifications. Concretely, we take a collection of JML-annotated programs, that we tried to reverify using KeY and OpenJML. This effort led to a list of syntactical and semantical differences in the JML support between KeY and OpenJML. We discuss these differences, and then derive some general principles on how to improve interoperability between verification tools, based on the experiences from this case study.
    Original languageEnglish
    Title of host publicationIntegrated Formal Methods
    Subtitle of host publication14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018. Proceedings
    EditorsCarlo A. Furia, Kirsten Winter
    Place of PublicationCham
    Number of pages17
    ISBN (Electronic)978-3-319-98938-9
    ISBN (Print)978-3-319-98937-2
    Publication statusPublished - 5 Sep 2018
    Event14th International Conference on Integrated Formal Methods, IFM 2018 - Maynooth University, Maynooth, Ireland
    Duration: 5 Sep 20187 Sep 2018

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference14th International Conference on Integrated Formal Methods, IFM 2018
    Abbreviated titleIFM 2018
    Internet address


    Dive into the research topics of 'Reasoning About JML: Differences Between KeY and OpenJML'. Together they form a unique fingerprint.

    Cite this