Formal Software Development Methods

Fall 2021 Edition

This course is dedicated to studying formal techniques for building reliable software. The course will first teach the mathematical foundations of formally representing programs as mathematical objects, and how to reduce program verification to a mathematical theorem. Using this foundation, we will introduce various abstractions, such as contract based programming, as a way of formally specifying properties of code that facilitates modular and reliable program development.

We will cover a range of program verification and bug-finding techniqes for sequential and more challenging programs (e.g., concurrent, non-deterministic, or probabilistic). The course will be a mixture of theory and practice: the students will study practical applications using tools that prove important properties, such as safety or termination, using abstraction based techniques, model-checking, and developing programs using contracts.



  • 8/31/2021: We posted Homework Quizz 2 on the Campuswire.

  • 8/31/2021: We posted Homework Quizz 1 on the Campuswire. Deadline: September 9th.

  • 8/26/2021: We will post the lecture video links on the Campuswire forum.

  • 8/26/2021: We set the Campuswire discussion up. Please email the TA if you did not get the invitation yet.

  • 8/22/2021: Zoom link for the lectures (Requires Illinois login).

  • 8/22/2021: The website is up!

 Online: Zoom link.
 Board: Campuswire.

 Sasa Misailovic
 Assistant Professor
 Computer Science, UIUC
 4110 Siebel Center
 Office hours upon request

 Vimuth Fernando
 Computer Science, UIUC
 3107 Siebel Center
 Office hours:
 Mon 11am-1pm (Zoom)


This is an advanced mixed undergraduate/graduate course. Undergraduate students take the 3-credit version of the course (out of 100 points). Graduate students take the 4-credit version of the course (out of 133 points; scaled to 100%). We will compute the final grade using the following table:

Activity Grade Details
Take-Home Quizzes 75 points
  • 4-5 Quizzes with Theoretical and Programming Assignments.
Take-Home Final Quizz 25 points
  • At the end of the semester.

For Graduate Students: 33 points
  • Project (individual or group of 2). Discuss the topic with the instructor before November 1.

More details about the course administration are available at the course logistics slides


Tentative Schedule  

Tentative Topics:

  • Background and Predicate Logic

  • Operational Program Semantics

  • Static Analysis and Abstract Interpretation

  • First Order Logic, Hoare Logic and Code Contracts

  • Model Checking

  • Advanced Topics

Date Topic Notes


Slides / Video

Background and Propositional Logic


Propositional Logic (continued)

Quizz 1 out - Check Forum.

Simple Imperative Programs, Syntax and Semantics (1)


Simple Imperative Programs, Operational Semantics (2)


Symbolic Execution

Quizz 2 out - Check Forum.

Dataflow analysis and abstract interpretation (1)


Dataflow analysis and abstract interpretation (2)


Dataflow analysis and abstract interpretation (3)


Dataflow analysis and abstract interpretation (4)

Part 1
Part 2