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.
12/10/2021: We posted the final exam.
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!
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 |
|
Take-Home Final Quizz | 25 points |
|
For Graduate Students: | 33 points |
|
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 ExecutionQuizz 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) |
Fall Break |
||
11/30 | Guest Lecture: Gagandeep Singh |
|
12/2 | Guest Lecture: Jacob Laurel and Vimuth Fernando |
|
12/7 | Student Presentations |