Reasoning About JML: Differences Between KeY and OpenJML

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

15 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

Specifications
Specification languages
Interoperability
Semantics
Formal verification

Cite this

Boerman, J., Huisman, M., & Joosten, S. J. C. (2018). Reasoning About JML: Differences Between KeY and OpenJML. In C. A. Furia, & K. Winter (Eds.), Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018. Proceedings (pp. 30-46). [3] (Lecture Notes in Computer Science; Vol. 11023). Cham: Springer. https://doi.org/10.1007/978-3-319-98938-9_3
Boerman, Jan ; Huisman, Marieke ; Joosten, Sebastiaan Jozef Christiaan. / Reasoning About JML: Differences Between KeY and OpenJML. Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018. Proceedings. editor / Carlo A. Furia ; Kirsten Winter. Cham : Springer, 2018. pp. 30-46 (Lecture Notes in Computer Science).
@inproceedings{58a1843536644a9a8de3003732791306,
title = "Reasoning About JML: Differences Between KeY and OpenJML",
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.",
author = "Jan Boerman and Marieke Huisman and Joosten, {Sebastiaan Jozef Christiaan}",
year = "2018",
month = "9",
day = "5",
doi = "10.1007/978-3-319-98938-9_3",
language = "English",
isbn = "978-3-319-98937-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "30--46",
editor = "Furia, {Carlo A.} and Kirsten Winter",
booktitle = "Integrated Formal Methods",

}

Boerman, J, Huisman, M & Joosten, SJC 2018, Reasoning About JML: Differences Between KeY and OpenJML. in CA Furia & K Winter (eds), Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018. Proceedings., 3, Lecture Notes in Computer Science, vol. 11023, Springer, Cham, pp. 30-46, 14th International Conference on Integrated Formal Methods, IFM 2018, Maynooth, Ireland, 5/09/18. https://doi.org/10.1007/978-3-319-98938-9_3

Reasoning About JML: Differences Between KeY and OpenJML. / Boerman, Jan; Huisman, Marieke ; Joosten, Sebastiaan Jozef Christiaan.

Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018. Proceedings. ed. / Carlo A. Furia; Kirsten Winter. Cham : Springer, 2018. p. 30-46 3 (Lecture Notes in Computer Science; Vol. 11023).

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

TY - GEN

T1 - Reasoning About JML: Differences Between KeY and OpenJML

AU - Boerman, Jan

AU - Huisman, Marieke

AU - Joosten, Sebastiaan Jozef Christiaan

PY - 2018/9/5

Y1 - 2018/9/5

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85053120169&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-98938-9_3

DO - 10.1007/978-3-319-98938-9_3

M3 - Conference contribution

SN - 978-3-319-98937-2

T3 - Lecture Notes in Computer Science

SP - 30

EP - 46

BT - Integrated Formal Methods

A2 - Furia, Carlo A.

A2 - Winter, Kirsten

PB - Springer

CY - Cham

ER -

Boerman J, Huisman M, Joosten SJC. Reasoning About JML: Differences Between KeY and OpenJML. In Furia CA, Winter K, editors, Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018. Proceedings. Cham: Springer. 2018. p. 30-46. 3. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-98938-9_3