This artifact [1] (accompanying our iFM 2023 paper [2]) describes the software we developed that contributed towards our analysis of OpenJDK's BitSet class. This class represents a vector of bits that grows as needed. Our analysis exposed numerous bugs. In our paper, we proposed and compared a number of solutions supported by formal specifications. Full mechanical verification of the BitSet class is not yet possible due to limited support for bitwise operations in KeY and bugs in BitSet. Our artifact contains proofs for a subset of the methods and new proof rules to support bitwise operators.

, , , ,
doi.org/10.1016/j.scico.2024.103232
Science of Computer Programming
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Tatman, A., Hiep, H.-D., & de Gouw, S. (2025). Analysis and formal specification of OpenJDK's BitSet: Proof files. Science of Computer Programming, 241. doi:10.1016/j.scico.2024.103232