2024-09-01
Analysis and formal specification of OpenJDK's BitSet: Proof files
Publication
Publication
The project files for the article: "Analysis and Formal Specification of OpenJDK's BitSet". The files contain: - The KeY 2.10.0 jar executable, which is the prover used in this verification. - A PDF of the article - The original version of OpenJDK's BitSet class. - Our edited version of the BitSet class, including formal specification and files necessary to load the code into KeY. - A folder containing a number of completed proofs for simple methods from the BitSet class, as well as proofs for statements made in the article.
| Additional Metadata | |
|---|---|
| doi.org/10.5281/zenodo.8043379 | |
| www.gnu.org/licenses/old-licenses/gpl-2.0.html | |
|
Tatman, A., Hiep, H.-D., & de Gouw, S. (2024). Analysis and formal specification of OpenJDK's BitSet: Proof files. doi:10.5281/zenodo.8043379 |
|
| Additional Files | |
|---|---|
| View at Zenodo | |
| See Also |
|---|
inProceedings
|