Tutorials & Examples
Load an example from the list presented in the dialog that pops up when starting KeY. Good choices are, e.g.:
- “Quicktour” for program verification
- “Transitivity of Subset” for first-order logic
- “Declassification – Sum” for information flow analysis
KeY as a Library
You can use KeY as a library in your own project: Make use of its capabilities as a first-order prover or symbolic execution engine. We provide some starting points for you in the “KeY for Your Own Research Projects” section.
Download the KeY nightly source code distribution here and have a look at our Javadoc documentation if you want to extend KeY or understand how things work under the hood.
The preferred way for getting help, in particular when you want to use KeY as a library or want to change or extend the source code, is to use StackOverflow. Be sure to tag your question with the key-formal-verification tag, so that your question is not lost amongst all the questions on StackOverflow.
Alternatively, you can write an email to our mailing list .