This collection of video material consists of screen recordings of interactive proof sessions with the KeY theorem prover. Each video displays how to create a proof for part of one method contract, or proofs of several method contracts. The method contracts are expressed in the Java Modeling Language with KeY-specific extensions (not shown in the video).

, ,
doi.org/10.6084/m9.figshare.c.4826589.v2
Computer Security

Bian, J., & Hiep, H.-D. (2020). A tutorial on verifying LinkedList using KeY: Video material. doi:10.6084/m9.figshare.c.4826589.v2