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.
The module has two major parts. In the first part we will focus on studying the fundamental properties that are unique to software systems and how they affect the development of such systems. In the second part we will focus on describing techniques that can help us to address the challenges that we have investigated in the first part. Throughout the module we will explore case studies of successful and failed software projects to demonstrate the theoretical analysis in practice. The students will work in small groups; each group will analyze a few case studies and present the result of their analysis to the class. The module's grade will consist of 50% presentation of the case study and 50% a final exam. The exam will include questions both on the theory and on the case studies.