Integrating ADTs in KeY and their Application to History-based Reasoning : Video Material

This is the collection of video material that used in "Integrating ADTs in KeY and their Application to History-based Reasoning". It contains screen recordings of interactive proof sessions with the KeY theorem prover. Each video displays how to create a proof for case study. The method contracts are expressed in the Java Modeling Language (not shown in the video).

We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and translate Isabelle theorems to user-defined taclets in KeY. As a case study of this new approach, we reason about Java's Collection interface using histories, and we prove the correctness of several clients that operate on multiple objects, thereby significantly improving the state-of-the-art of history-based reasoning.