Analysis and Formal Specification of OpenJDK's BitSet
The work
| Authors | Andy S. Tatman; Hans-Dieter A. Hiep; Stijn de Gouw |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2024 |
| Also known as | tatman2023analysis |
| Citekey | tatman2024analysis |
Where it appeared
| Published in | Integrated Formal Methods |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 14300 |
| Pages | 134--152 |
Identifiers
| DOI | 10.1007/978-3-031-47705-8_8 |
|---|---|
| OpenAlex | W4388573797 |
Access
| Landing page | https://doi.org/10.1007/978-3-031-47705-8_8 |
|---|---|
| Free full text | https://scholarlypublications.universiteitleiden.nl/access/item%3A3766076/view |
Related
| Distinct from | kar2013mosfet |
|---|---|
| Distinct from | meyer1991design |
Abstract
This paper uses a combination of formal specification and testing, to analyse OpenJDK’s BitSet class. This class represents a vector of bits that grows as required. During our analysis, we uncovered a number of bugs. We propose and compare various solutions, supported by our formal specification. While a full mechanical verification of the BitSet class is not yet possible due to limited support for bitwise operations in the KeY theorem prover, we show initial steps taken to formally verify the challenging get(int,int) method, and discuss some required extensions to the theorem prover.
A copy is held
pdf, 476.5 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-18 16:22 UTC |
Filed under
Cite it as
@inproceedings{tatman2024analysis,
title = {Analysis and Formal Specification of OpenJDK's BitSet},
author = {Andy S. Tatman and Hans-Dieter A. Hiep and Stijn de Gouw},
year = {2024},
booktitle = {Integrated Formal Methods},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {134--152},
doi = {10.1007/978-3-031-47705-8_8},
}
This record lives at https://refs.drheap.org/tatman2024analysis/ and will keep
doing so. It used to be called tatman2023analysis, and those addresses still resolve to this one.