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

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