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: 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:
|Take-Home Quizzes||75 points||
|Take-Home Final Quizz||25 points||
|For Graduate Students:||33 points||
Background and Predicate Logic
Operational Program Semantics
Static Analysis and Abstract Interpretation
First Order Logic, Hoare Logic and Code Contracts
|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)
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)