This module teaches the theory and practice of formally proving the correctness of imperative sequential programs using the Dafny formal verification language and tool set.
The module consists of two parts. In the first part we will study simple reactive systems and learn how to model them as transition systems and how to express properties using temporal logic formulas. We will then learn how to use a model checker to check if the models satisfy the properties. In the second part we will learn how to describe information systems using relational logic and how to express business rules and structural invariants using relational logic formulas. Finally, we will learn how to use the Alloy analyzer to check that the model satisfies the business rules and structural invariants.
