Analysis and Formal Specification of OpenJDK's BitSet

The work

TitleAnalysis and Formal Specification of OpenJDK's BitSet
AuthorsAndy S. Tatman; Hans-Dieter A. Hiep; Stijn de Gouw
Typeconference paper
Year2024
Also known astatman2023analysis
Citekeytatman2024analysis

Where it appeared

Published inIntegrated Formal Methods
PublisherSpringer
SeriesLecture Notes in Computer Science
Number in series14300
Pages134--152

Identifiers

DOI10.1007/978-3-031-47705-8_8
OpenAlexW4388573797

Access

Landing pagehttps://doi.org/10.1007/978-3-031-47705-8_8
Free full texthttps://scholarlypublications.universiteitleiden.nl/access/item%3A3766076/view

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.

Copy held

KindPDF, 487.9 kB
Retrieved2026-08-08
Heldlocal, for personal reference
Opens atpage 2
Where it came fromhttps://scholarlypublications.universiteitleiden.nl/access/item%3A3766076/view

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-04
Recordreviewed by a person
Approved2026-08-18
In: Integrated Formal Methods (iFM) venue Lecture Notes in Computer Science series Verifying real Java topic

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},
  pages = {134--152},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {14300},
  doi = {10.1007/978-3-031-47705-8_8},
  url = {https://scholarlypublications.universiteitleiden.nl/access/item%3A3766076/view},
}

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.