KeY for Your Own Research Projects

This page is under construction

  • 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.