History-Based Specification and Verification of Java Collections in KeY

Hans-Dieter A. Hiep, Jinting Bian, Frank S. de Boer, Stijn de Gouw

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


In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java’s Collection interface. We introduce a new specification method (in the KeY theorem prover) using histories, that record method invocations including their parameters and return value, on an interface. We outline the challenges of proving client code correct with respect to arbitrary implementations, and describe a practical specification and verification effort of part of the Collection interface using KeY (including source and video material).
Original languageEnglish
Title of host publicationIntegrated Formal Methods
Subtitle of host publication16th International Conference, IFM 2020
EditorsBrijesh Dongol, Elena Troubitsyna
Place of PublicationLugano, Switzerland
Number of pages19
ISBN (Electronic)978-3-030-63461-2
ISBN (Print)978-3-030-63461-2
Publication statusPublished - 13 Nov 2020
Event16th international conference, Integrated Formal Methods 2020 - Online, Lugano, Switzerland
Duration: 16 Nov 202020 Nov 2020
Conference number: 16

Publication series

SeriesLecture Notes in Computer Science


Conference16th international conference, Integrated Formal Methods 2020
Abbreviated titleIFM 2020
Internet address

Fingerprint Dive into the research topics of 'History-Based Specification and Verification of Java Collections in KeY'. Together they form a unique fingerprint.

Cite this