- 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
The following code snippet shows how to access the symbolic execution API programmatically.
Relevant blog posts
How researchers from UPM and IMDEA used KeY as backend - Researchers (Julio Mariño Raúl, N. N. Alborodo, Lars-Åke Fredlund and Ángel Herranz) from UPM and IMDEA (both Madrid, Spain) developed a methodology to synthesize verifiable concurrent Java components from formal models.