2020
A tutorial on verifying LinkedList using KeY: Proof files
Publication
Publication
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/LinkedList.java)
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.
| Additional Metadata | |
|---|---|
| Formal methods, Deductive verification, KeY project, Java Modeling Language, java.util.LinkedList | |
| dx.doi.org/10.5281/zenodo.3613712 | |
| Organisation | 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
|
|
