The project files for the article `A Tutorial on Verifying LinkedList using KeY'. The archive contains:

A bundled version of KeY, version 2.6.3. This requires a recent version of Java Runtime Edition (JRE) to be executed, say OpenJDK8.

A number of stub contracts (jre/ directory).

A skeleton LinkedList source file (src/java/util/LinkedList.old) for the reader of the tutorial to fill in the methods and contracts.

The LinkedList source file after all modifications have been done (src/java/util/

A number of proof files that can be loaded in KeY, that verify the correctness of the methods with respect to their contract as given in the solution.

Formal methods, Deductive verification, KeY project, Java Modeling Language, java.util.LinkedList
Computer Security

Hiep, H.A, Bian, J, de Boer, F.S, & de Gouw, C.P.T. (2020). A tutorial on verifying LinkedList using KeY: Proof files. doi:10.5281/zenodo.3613712