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

    44 Downloads (Pure)

    Abstract

    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
    PublisherSpringer
    Pages30-46
    Number of pages17
    ISBN (Electronic)978-3-319-98938-9
    ISBN (Print)978-3-319-98937-2
    DOIs
    Publication statusPublished - 5 Sep 2018
    Event14th International Conference on Integrated Formal Methods, IFM 2018 - Maynooth University, Maynooth, Ireland
    Duration: 5 Sep 20187 Sep 2018
    https://ifm2018.cs.nuim.ie/

    Publication series

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

    Conference

    Conference14th International Conference on Integrated Formal Methods, IFM 2018
    Abbreviated titleIFM 2018
    CountryIreland
    CityMaynooth
    Period5/09/187/09/18
    Internet address

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

    Cite this