Students will learn about models of computing machines: finite automata, pushdown automata, and Turing machines. Students will demonstrate knowledge of Formal languages, their descriptions, and their relationships to the computational models; Students will learn the limits of the various models.
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.