Formal Methods for Software Development

Exercises Week 7 – Dynamic Logic

These are the exercises for week 7.

Here are some dynamic logic programs. Play around with KeY and get to know how KeY works to verify dynamic logic problems. If some programs cannot be verified, think about the reasons and fix them.

Here are some suggestions on how the KeY files can be modified to make the problems described by them provable.

W. Ahrendt, Oct 18, 2019