Analysis and formal specification of OpenJDK's BitSet: Proof files

Andy S. Tatman; Hans Dieter A. Hiep; Stijn de Gouw

doi:10.1016/j.scico.2024.103232

Analysis and formal specification of OpenJDK's BitSet: Proof files

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

^*Corresponding author for this work

Research output: Contribution to journal › Article › Academic › peer-review

Abstract

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.

Original language	English
Article number	103232
Journal	Science of Computer Programming
Volume	241
DOIs	https://doi.org/10.1016/j.scico.2024.103232
Publication status	Published - Apr 2025

Keywords

Formal specification
Java/OpenJDK
JML
KeY
Testing

Access to Document

10.1016/j.scico.2024.103232

Cite this

@article{821da7340a844779959cbd9500564cff,

title = "Analysis and formal specification of OpenJDK's BitSet: Proof files",

abstract = "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.",

keywords = "Formal specification, Java/OpenJDK, JML, KeY, Testing",

author = "Tatman, {Andy S.} and Hiep, {Hans Dieter A.} and {de Gouw}, Stijn",

note = "Publisher Copyright: {\textcopyright} 2024 Elsevier B.V.",

year = "2025",

month = apr,

doi = "10.1016/j.scico.2024.103232",

language = "English",

volume = "241",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Analysis and formal specification of OpenJDK's BitSet

T2 - Proof files

AU - Tatman, Andy S.

AU - Hiep, Hans Dieter A.

AU - de Gouw, Stijn

PY - 2025/4

Y1 - 2025/4

N2 - 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.

AB - 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.

KW - Formal specification

KW - Java/OpenJDK

KW - JML

KW - KeY

KW - Testing

U2 - 10.1016/j.scico.2024.103232

DO - 10.1016/j.scico.2024.103232

M3 - Article

AN - SCOPUS:85209390389

SN - 0167-6423

VL - 241

JO - Science of Computer Programming

JF - Science of Computer Programming

M1 - 103232

ER -

Analysis and formal specification of OpenJDK's BitSet: Proof files

Abstract

Keywords

Access to Document

Fingerprint

Cite this