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.

Teams of 1 are accepted but not encouraged.

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 in TLA+

  • Expressing fairness and liveness in TLA+

  • Satisfiability Modulo Theories (SMT) solvers

  • 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

Time permitting, possible additional topics might include:

  • Modelling concurrency in Dafny

  • 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: 60%

    • Homework 1: TLA+: 20%

    • Homework 2: SMT: 20%

    • Homework 3: Dafny: 20%

  • Research Project: 40%.

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

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

    • 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.