A Tutorial on Verifying LinkedList using KeY: Video Material
Jinting Bian, Hans-Dieter A. Hiep · Data Archiving and Networked Services (DANS) · 2020
This collection of video material consists of screen recordings of interactive proof sessions with the KeY theorem prover. Each video displays how to create a proof for part of one method contract, or proofs of several method contracts. The method contracts are expressed in the Java Modeling Language with KeY-specific extensions (not shown in the video).