KeY Version for IJCAR submission (For IJCAR 2018 Reviewers Only)
Download or Start
KeY requires Java version 8 or newer and is tested on Linux, OS X and Microsoft Windows.
- Instant Start: Web Start
- Binary Version: KeY
- Source Code: KeY-src.zip
- The technical report contains more material than could be covered in the page resticted paper.
- The following zip-files contain proofs of the lemmas contained in the IJCAR submission Proofs1 Proofs2 The files in these zip-archives use KeY internal names. The correspondence between the lemma whose proof you want to inspect and the name of the proof file can be retrieved from Fml2Taclet. To inspect the proofs, start the KeY system and select in the pull-down menue “file” subitem “load” t he wanted proof file. Proof files come with extensions .key or .proof. The user will not note any difference after loading them. The .proof files contain saved finished proofs. The .key files contain commands of a simple, experimental scripting language that construct the proof on the fly.
[button type=”primary” size=”lg” link=”http://formal.iti.kit.edu/key/floc-2018-pschmitt/webstart/KeY.jnlp”][icon type=”play”] Run KeY via Webstart [/button]