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.

 

News  

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


 Lectures:
 Tuesday/Thursday
 11:00am-12:15pm
 Online: Zoom link.
 Board: Campuswire.

 Instructor:
 Sasa Misailovic
 Assistant Professor
 Computer Science, UIUC
 4110 Siebel Center  misailo@illinois.edu
 Office hours upon request

 TA:
 Vimuth Fernando
 Computer Science, UIUC
 3107 Siebel Center  wvf2@illinois.edu
 Office hours:
 Mon 11am-1pm (Zoom)

Overview  

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
8/24

Introduction


Slides / Video
8/26

Background and Propositional Logic


Slides
8/31

Propositional Logic (continued)


Quizz 1 out - Check Forum.
Slides
9/2

Simple Imperative Programs, Syntax and Semantics (1)


Slides
9/7

Simple Imperative Programs, Operational Semantics (2)


Slides
9/9

Symbolic Execution


Quizz 2 out - Check Forum.
Slides
9/14

Dataflow analysis and abstract interpretation (1)


Slides
9/16

Dataflow analysis and abstract interpretation (2)


Slides
9/21

Dataflow analysis and abstract interpretation (3)


Slides
9/23

Dataflow analysis and abstract interpretation (4)


Slides
9/28

Dataflow analysis and abstract interpretation (5)


Slides
9/30

Dataflow analysis and abstract interpretation (6)


Slides
10/5

First Order Logic (1)


Slides
10/7

First Order Logic (2)


Slides
10/12

First Order Logic (3)


Slides
10/14

Hoare Logic (1)


Slides
10/19

Hoare Logic (2)


Slides
10/21

Hoare Logic (3)


Slides
(See also the video for Vimuth's demo)
10/26

Reasoning About Pointers


Slides
10/28

Reasoning About Termination


Slides
11/2

Model Checking (1)


Slides
11/4

Model Checking (2)


Slides
11/9

Model Checking (3)


Materials
(See also the video for Vimuth's demo)
11/11

Model Checking: Concurrency


Slides
(See also the video for Vimuth's demo)