A tutorial on verifying LinkedList using KeY: Video material

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)