This is a tutorial paper on using KeY to demonstrate formal verification of state-of-the-art, real software. In sufficient detail for a beginning user of JML and KeY, the specification and verification of part of a corrected version of the java.util.LinkedList class of the Java Collection framework is explained. The paper includes video material that shows recordings of interactive sessions, and project files with solutions. As such, this material is also interesting for the expert user and the developer of KeY as a ‘benchmark’ for specification and (automatic) verification techniques.
|Title of host publication||Deductive Software Verification|
|Subtitle of host publication||Future Perspectives|
|Editors||Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich|
|Place of Publication||Cham|
|Number of pages||25|
|Publication status||Published - 2020|
|Series||Lecture Notes in Computer Science|