Formal Specification and Analysis of OpenJDK's BitSet class: Proof files

Zenodo (CERN European Organization for Nuclear Research)

Abstract

The project files for the bachelors thesis: "Formal Specification and Analysis of OpenJDK's BitSet class:". The files contain: The KeY 2.10.0 jar executable, which is the prover used in this verification. A PDF of the thesis. 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 Proof folder containing: A number of completed proofs for simple methods from the BitSet class. Proofs of more complex methods from the BitSet class, including videos of these proofs being performed. Proofs for statements made in the thesis Proof goals and completed proofs for rules used in verification.

Authors 1

1. Andy S. Tatman corresponding Aachen Leiden Institute of Advanced Computer Science

   Leiden University

   Affiliation as printed

   Leiden Institute of Advanced Computer Science (LIACS)