KeY

Please watch the introduction video (no audio). You can pause the video at any time to comprehend the content. Click here, if you want to open the example of the video in KeY (external window).

Best Practices

  1. Focus on a goal.
  2. Inspect the parent nodes of the goal to comprehend
    1. the followed execution path.
    2. the parts of the postcondition which
      1. could be proven and
      2. are currently still open.