Tutorials & ExamplesLoad 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 LibraryYou 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.