History-based Specification and Verification of Java Collections in KeY: Proof Files

This repository consists of the proof files for the paper "History-based Specification and Verification of Java Collections in KeY". It contains the KeY version used, an overview of the proof statistics (as it occurs in the paper), and all produced proof files in the Proof folder. Running KeY needs a Java runtime, e.g. OpenJDK version 1.8.0_242 or any later compatible version.

Abstract: In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java's Collection interface. We introduce a new specification method (in KeY) using histories, that records method invocations and their parameters on an interface. We outline the challenges of proving client code correct with respect to arbitrary implementations, and describe a practical specification and verification effort of part of the Collection interface using KeY (including source and video material).