2025-04-01
Analysis and formal specification of OpenJDK's BitSet: Proof files
Publication
Publication
Science of Computer Programming , Volume 241
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.
| Additional Metadata | |
|---|---|
| , , , , | |
| doi.org/10.1016/j.scico.2024.103232 | |
| Science of Computer Programming | |
| Organisation | 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 |
|