Verifying OpenJDK’s LinkedList using KeY By Hans-Dieter Hiep

There is a bug in Java's LinkedList. In this technical demo session, the KeY theorem prover is shown in action, as we walk through verification of some methods of a repaired LinkedList implementation, and explain the most interesting steps of its correctness proof.