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.

, , , ,
Lecture Notes in Computer Science
The 18th International Conference on integrated Formal Methods, iFM 2023
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Tatman, A., Hiep, H.-D., & de Gouw, S. (2024). Analysis and formal specification of OpenJDK’s BitSet. In Integrated Formal Methods (pp. 134–152). doi:10.1007/978-3-031-47705-8_8