Deductive verification case study in which we formally verify [Java's IdentityHashMap]
(http://hg.openjdk.java.net/jdk7u/jdk7u/jdk/file/4dd5e486620d/src/share/classes/java/util/IdentityHashMap.java).
We used the Java Modeling Language JML for formal specification
and KeY as interactive theorem prover.
We used JJBMC and JUnit to gain
confidence while engineering the specification.
The specified sources code can be found in the following 4 repositories:
- IM9906-2-VerifyingIdentityHashMap
contains the JML specification and the
KeY proof files for every proven method. It also contains
the binary of the KeY tool that was used to formally verify the
IdentityHashMap. - IM9906-2-IdentityHashMapSpecTester contains the JUnit tests to gain confidence during the specification engineering process.
- HashTableWithKeY contains the sources of a case study in which we looked at collision resolution strategies in relation to formal verification with KeY.
- JJBMC contains the JJBMC codebase. JJBMC is a tool which enables the software bounded model checker JBMC to verify contracts written in JML.
A report on the case study is currently under review.