Exercises Week 6 – Dynamic Logic

These are the exercises for week 6.

Here are some dynamic logic sequents for KeY. The purpose of this exercise is to understand both dynamic logic, as well as how KeY works to verify these problems.

We do so by discussing the sequents in the session. Some of the sequents can not be proven by KeY and we should reason how we can modify them so that they become provable.

The collection of .key-files might be slightly changed in the days before the session to give a good overview of the various features of KeY and dynamic logic.