Thursday 17 October 2019 15:45 - 16:30
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.
