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

Abstract

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
PublisherSpringer
Pages199-217
Number of pages19
ISBN (Electronic)978-3-030-63461-2
ISBN (Print)978-3-030-63461-2
DOIs
Publication statusPublished - 13 Nov 2020
Event16th international conference, Integrated Formal Methods 2020 - Online, Lugano, Switzerland
Duration: 16 Nov 202020 Nov 2020
Conference number: 16
https://ifm20.si.usi.ch/

Publication series

SeriesLecture Notes in Computer Science
ISSN0302-9743

Conference

Conference16th international conference, Integrated Formal Methods 2020
Abbreviated titleIFM 2020
Country/TerritorySwitzerland
CityLugano
Period16/11/2020/11/20
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