A tutorial on verifying LinkedList using KeY: Proof files
- Hiep, H.A. (Hans-Dieter)
- Bian, J. (Jinting)
- Boer, F.S. (Frank) de
- Gouw, C.P.T. (Stijn) de
Publication date
January 2020
DOIAbstract
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.</p
Add to ORKG