2024
Analysis and formal specification of OpenJDK’s BitSet
Publication
Publication
Presented at the
The 18th International Conference on integrated Formal Methods, iFM 2023 (November 2023), Leiden, The Netherlands
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.
| Additional Metadata | |
|---|---|
| , , , , | |
| doi.org/10.1007/978-3-031-47705-8_8 | |
| Lecture Notes in Computer Science | |
| The 18th International Conference on integrated Formal Methods, iFM 2023 | |
| Organisation | 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 |
|