History-Based Specification and Verification of Java Collections in KeY
The work
| Authors | Hans-Dieter A. Hiep; Jinting Bian; Frank S. de Boer; Stijn de Gouw |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2020 |
| Citekey | hiep2020historybased |
Where it appeared
| Published in | Integrated Formal Methods |
|---|---|
| Publisher | Springer |
| Pages | 199--217 |
Identifiers
| DOI | 10.1007/978-3-030-63461-2_11 |
|---|---|
| OpenAlex | W3100554104 |
Access
| Landing page | https://doi.org/10.1007/978-3-030-63461-2_11 |
|---|---|
| Free full text | https://ir.cwi.nl/pub/29970/29970.pdf |
Abstract
In this feasibility study we discuss reasoning about the cor- rectness 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).
A copy is held
pdf, 292.0 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-12 14:58 UTC |
Filed under
bian deboer degouw hiep ifm lncs the-copy-is-not-the-work verifying-real-java
Cite it as
@inproceedings{hiep2020historybased,
title = {History-Based Specification and Verification of Java Collections in KeY},
author = {Hans-Dieter A. Hiep and Jinting Bian and Frank S. de Boer and Stijn de Gouw},
year = {2020},
booktitle = {Integrated Formal Methods},
publisher = {Springer},
pages = {199--217},
doi = {10.1007/978-3-030-63461-2_11},
}
This record lives at https://refs.drheap.org/hiep2020historybased/ and will keep doing so.