KeY for Your Own Research Projects

  • 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

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.