Course Syllabus and Policies

Goals of the Course

This course provides an introduction to practical applications formal methods for specifying and designing software systems. The purpose of formal methods is to enable the construction of highly reliable software. Formal methods are concerned with specifications that are precise for being stated in languages endowed with a formal syntax, and semantics (i.e., precise meaning). Formality helps the specification process in at least two ways:

  1. it delivers unambiguous, high-quality specifications, and

  2. it enables automated tool support.

As we will see, formal specification techniques allow for using state-of-the-art tools for automated validation and verification that help software developers make sense of the specifications and the corresponding code, looking for errors in requirements, models, designs, and implementations.

In this course, we will study a collection of techniques for formal software development, spanning the whole development process: from high-level semantic modeling of a system’s behaviour to verifying that its implementation does what is intended. This study will be done through the use of actual tools supporting these techniques.

You are expected to put in considerable time and effort into working on the homework exercises and projects to gain experience with the techniques seen in class.

Homework Assignments and Projects

For each main topic there will be an individual homework assignment, contributing to the final grade as per the schema below.

In addition to the assignments, there will be a course project on the topic of software specification and verification. The projects will be done in teams of one or two students and will contribute a significant portion of the grade. Some high-level ideas for the projects will be offered around the third week of the class. The whole team is responsible for the work submitted. Although the work is shared, each student will received an individual grade. Team members will be asked to submit an evaluation of how well they and their teammates performed as team members. Each evaluation is confidential and will be be incorporated into the calculation of the individual grade.

Each student is responsible for contacting other students and form a team. The Slack channel dedicated t othe module can be use to establish initial contacts. Teams of 1 are accepted but not encouraged.

Late Submission Policy

Any assignment submitted after the deadline, up to 48 hours late, will be penalised by 20% of its maximal grade. Submissions made after 48 hours past the deadline, won’t be assessed and will get 0 points.

Topics and Lectures

The list of topics below is a subject of possible minor changes.

  • Introduction to Formal Methods for Software Engineering

  • Basic applications of TLA+, Z3, and Dafny

  • State-Transition Systems, Safety and Liveness Properties

  • Specifying and checking systems in TLA+

  • Verifying basic distributed protocols (Two-Phase Commit, Paxos) in TLA+

  • Fairness, liveness, and state machine refinement in TLA+

Mid-term break

  • Basics of Boolean satisfiability (SAT) solvers

  • Satisfiability Modulo Theories (SMT) solvers

  • A tour of SMT solver internals

  • Encoding simple verification and synthesis problems in SMT

  • Program verificaiton in Hoare logic

  • Introduction to Dafny

  • Specifying and verifying imperative programs in Hoare logic

  • Reasoning about loops, iterative and divide & conquer algorithms

  • Object invariants; verifying programs with arrays

  • Modelling concurrency in Dafny

Possible additional topics might include:

  • Decidable verification of distributed protocols

  • Separation Logic and verifying programs with pointers

  • Deductive synthesis of imperative programs

Grading Schema

The final grade is combined from the following components:

  • Homework Assignments: 30%

    • Homework 1: TLA+: 10%

    • Homework 2: SAT and SMT: 10%

    • Homework 3: Dafny: 10%

  • Theory Quizzes: 30%

    • Quiz 1 (Week 7, 1 hour): First-Order Logic and TLA+: 15%

    • Quiz 2 (Week 12, 1 hour): SAT, SMT, and Deductive Verification: 15%

  • Research Project: 40%.

    • Initial project proposal: 5% (why the problem is interesting, why feasible)

    • Code quality: 5% (well-documented, corresponds to the text in the report)

    • Written report: 10% (evaluated based on structure, clarity)

    • Presentation: 10% (you should be able to explain your design choices)

    • Self- and peer evaluation: 10% (based on the peer feedback in case of teams of two)

The following cutoffs will be used to determine letter grades. In the ranges below, x stands for your total score at the end of the semester. Final scores near a cutoff will be individually considered for the next higher grade. Plus(+) and minus(-) grades will also be given; their cutoffs will be determined at the end of the semester.

Score

Grade

88 ≤ x < 100

A

75 ≤ x < 88

B

60 ≤ x < 75

C

50 ≤ x < 60

D

0 ≤ x < 50

F

Grades are not curved. It is theoretically possible for everyone in the class to get an A (or an F). Your final grade depends only on your own final score and not on that of others.