- KeY’s symbolic execution API: The source code version includes the project key.core.symbolic_execution.example which provides a usage example of KeY’s symbolic execution engine.
- Verifying with KeY: The source code version includes the project key.core.example which creates all proof obligations for a given Java project and tries to verify them automatically using KeY’s prover.
Source code sample: Symbolic Execution API
The following code snippet shows how to access the symbolic execution API programmatically.
Source code sample: Program verification
The following code snippet shows how to programatically prove a program correct, i.e., by calling KeY from inside source code rather then using the CLI/GUI.
Relevant blog posts