Skip to Content

Reasoning About JML: Differences Between KeY and OpenJML

Posted on

Authors:

  • Boerman, Jan
  • Huisman, Marieke
  • Joosten, Sebastiaan J. C.

Published in: iFM 2018, LNCS. Furia, Carlo A. Winter, Kirsten (Eds) pp 1–17

Paper

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.

BibTeX entry:

@inproceedings{Boerman18,
 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},
 booktitle = {iFM 2018, LNCS},
 day = {5},
 editor = {Furia, {Carlo A.} and Kirsten Winter},
 language = {English},
 month = {9},
 pages = {1--17},
 title = {Reasoning About JML: Differences Between KeY and OpenJML},
 volume = {11023},
 year = {2018}
}