Analysis and Formal Specification of OpenJDK's BitSet

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

doi:10.1007/978-3-031-47705-8_8

Analysis and Formal Specification of OpenJDK's BitSet

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

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

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.

Original language	English
Title of host publication	iFM 2023 - 18th International Conference, iFM 2023, Proceedings
Subtitle of host publication	18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings
Editors	Paula Herber, Anton Wijs
Publisher	Springer
Pages	134-152
Number of pages	19
ISBN (Electronic)	9783031477058
ISBN (Print)	9783031477041
DOIs	https://doi.org/10.1007/978-3-031-47705-8_8
Publication status	Published - 2024
Event	18th International Conference on integrated Formal Methods - Leiden, Netherlands Duration: 13 Nov 2023 → 15 Nov 2023 https://ifm23.liacs.nl/

Publication series

Series	Lecture Notes in Computer Science
Volume	14300
ISSN	0302-9743

Conference

Conference	18th International Conference on integrated Formal Methods
Abbreviated title	iFM 2023
Country/Territory	Netherlands
City	Leiden
Period	13/11/23 → 15/11/23
Internet address	https://ifm23.liacs.nl/

Access to Document

10.1007/978-3-031-47705-8_8

Cite this

Tatman, A. S., Hiep, H.-D. A., & Gouw, S. D. (2024). Analysis and Formal Specification of OpenJDK's BitSet. In P. Herber, & A. Wijs (Eds.), iFM 2023 - 18th International Conference, iFM 2023, Proceedings: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings (pp. 134-152). Springer. https://doi.org/10.1007/978-3-031-47705-8_8

Tatman, Andy S. ; Hiep, Hans-Dieter A. ; Gouw, Stijn de. / Analysis and Formal Specification of OpenJDK's BitSet. iFM 2023 - 18th International Conference, iFM 2023, Proceedings: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. editor / Paula Herber ; Anton Wijs. Springer, 2024. pp. 134-152 (Lecture Notes in Computer Science, Vol. 14300).

@inproceedings{69523a2a2a47412a8a4e1a92afc630ff,

title = "Analysis and Formal Specification of OpenJDK's BitSet",

abstract = "This paper uses a combination of formal specification and testing, to analyse OpenJDK{\textquoteright}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.",

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

note = "DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.; 18th International Conference on integrated Formal Methods , iFM 2023 ; Conference date: 13-11-2023 Through 15-11-2023",

year = "2024",

doi = "10.1007/978-3-031-47705-8_8",

language = "English",

isbn = "9783031477041",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "134--152",

editor = "Paula Herber and Anton Wijs",

booktitle = "iFM 2023 - 18th International Conference, iFM 2023, Proceedings",

url = "https://ifm23.liacs.nl/",

}

Tatman, AS, Hiep, H-DA & Gouw, SD 2024, Analysis and Formal Specification of OpenJDK's BitSet. in P Herber & A Wijs (eds), iFM 2023 - 18th International Conference, iFM 2023, Proceedings: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. Springer, Lecture Notes in Computer Science, vol. 14300, pp. 134-152, 18th International Conference on integrated Formal Methods , Leiden, Netherlands, 13/11/23. https://doi.org/10.1007/978-3-031-47705-8_8

Analysis and Formal Specification of OpenJDK's BitSet. / Tatman, Andy S.; Hiep, Hans-Dieter A.; Gouw, Stijn de.
iFM 2023 - 18th International Conference, iFM 2023, Proceedings: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. ed. / Paula Herber; Anton Wijs. Springer, 2024. p. 134-152 (Lecture Notes in Computer Science, Vol. 14300).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Analysis and Formal Specification of OpenJDK's BitSet

AU - Tatman, Andy S.

AU - Hiep, Hans-Dieter A.

AU - Gouw, Stijn de

N1 - DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

PY - 2024

Y1 - 2024

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

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

U2 - 10.1007/978-3-031-47705-8_8

DO - 10.1007/978-3-031-47705-8_8

M3 - Conference Article in proceeding

SN - 9783031477041

T3 - Lecture Notes in Computer Science

SP - 134

EP - 152

BT - iFM 2023 - 18th International Conference, iFM 2023, Proceedings

A2 - Herber, Paula

A2 - Wijs, Anton

PB - Springer

T2 - 18th International Conference on integrated Formal Methods

Y2 - 13 November 2023 through 15 November 2023

ER -

Tatman AS, Hiep HDA, Gouw SD. Analysis and Formal Specification of OpenJDK's BitSet. In Herber P, Wijs A, editors, iFM 2023 - 18th International Conference, iFM 2023, Proceedings: 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings. Springer. 2024. p. 134-152. (Lecture Notes in Computer Science, Vol. 14300). doi: 10.1007/978-3-031-47705-8_8

Analysis and Formal Specification of OpenJDK's BitSet

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this