Analysis and Formal Specification of OpenJDK's BitSet

Andy S. Tatman*, Hans-Dieter A. Hiep, Stijn de Gouw

*Corresponding author for this work

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


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.
Original languageEnglish
Title of host publicationiFM 2023 - 18th International Conference, iFM 2023, Proceedings
Subtitle of host publication18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings
EditorsPaula Herber, Anton Wijs
Number of pages19
ISBN (Electronic)9783031477058
ISBN (Print)9783031477041
Publication statusPublished - 2024
Event18th International Conference on integrated Formal Methods - Leiden, Netherlands
Duration: 13 Nov 202315 Nov 2023

Publication series

SeriesLecture Notes in Computer Science


Conference18th International Conference on integrated Formal Methods
Abbreviated titleiFM 2023
Internet address


Dive into the research topics of 'Analysis and Formal Specification of OpenJDK's BitSet'. Together they form a unique fingerprint.

Cite this