SPRING 2024 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 bugfinding techniques for sequential and more challenging programs (e.g., concurrent, nondeterministic, 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, modelchecking, and developing programs using contracts.
Please note that this is an inperson class. Attendance will not be recorded in the first two weeks. We will start tracking attendance starting the third week. If you're unable to attend a class, please notify the instructor with a valid reason.
4/11/2024: Homework 5 is release on Gradescope. Due 11:59PM on 4/19
4/8/2024: Homework 4 is extened to today at 11:59PM
4/5/2024: Homework 4 is due 11:59PM
3/28/2024: Homework 4 is release on Gradescope
2/29/2024: Homework 3 is release on Gradescope
2/29/2024: Professor Singh's Office Hour Changed from 2pm to 5:30pm on Thursday.
2/15/2024: Homework 2 is release on Gradescope
2/7/2024: Homework 1 is due at 11:59 PM.
1/31/2024: Homework 1 is release on Gradescope
1/15/2024: The website is up!
This is an advanced mixed undergraduate/graduate course. Undergraduate students take the 3credit version of the course (out of 100 points). Graduate students take the 4credit version of the course (out of 125 points; scaled to 100%). We will compute the final grade using the following table:
Activity  Grade  Details 

Homeworks  90 pts 

Attendance  10 pts 

For Graduate Students:  25 pts 

We will use Gradescope for homework submissions. The Gradescope invitation code is VB7YB5. Please enroll in the course using this code.
We will use Campuswire for course announcements and discussions. Please enroll in the course using the code 7251.
Each student has a total of four additional days throughout the term to accommodate late submissions for homework assignments. This cumulative allowance can be used at the your discretion across different assignments.
If you submit more than 5 minutes late for an assignment, then it is considered as using one full day of the late submission allowance.
Once you exhaust the fourday late submission allowance, any further late homework submissions will result in a penalty of 33% grade reduction / day.
Tentative Topics:
Background
Operational Program Semantics
Static Analysis and Abstract Interpretation
Predicate Logic, First Order Logic, Hoare Logic and Code Contracts
Model Checking
Advanced Topics
Date  Topic  Notes 

1/15  Lecture 1. Course Introduction 
Slides / Video 
1/18  Lecture 2. Backgrounds 
Slides / Video 
1/18  Lecture 3. Cancelled due to Inclement Weather 

1/25  Lecture 4. Backgrounds Continued & ControlFlow Graph 
Slides (Same as Lecture 2) / Video 
1/30  Lecture 5. Operational Semantics 
Slides (Same as Lecture 2) / Video 
2/1  Lecture 6. Operational Semantics Continued 
Slides / Video 
2/6  Lecture 7. Intro to Symbolic Execution 
Slides / Video 
2/8  Lecture 8. Symbolic Execution Continued 
Slides / Video 
2/13  Lecture 9. Static Analysis 
Slides / Video 
2/15  Lecture 10. Static Analysis Continued 
Slides / Video 
2/20  Lecture 11. Static Analysis Continued 
Slides / Video 
2/22  Lecture 12. Static Analysis Continued 
Slides / Video 
2/27  Lecture 13. Data Flow Analysis 
Slides / Video 
2/29  Lecture 14. Data Flow Analysis. 
Slides / Video 
3/5  Lecture 15. Data Flow Analysis. 
Slides / Video 
3/7  Lecture 16. Abstract Interpretation. 
Slides / Video 
3/19  Lecture 17. Abstract Interpretation. 
Slides / Video 
3/21  Lecture 18. Abstract Interpretation. 
Slides / Video 
3/26  Lecture 19. Propositional Logics. 
Slides / Video 
3/28  Lecture 19. First Order Logics. 
Slides / Video 
4/2  Lecture 20. First Order Logics. 
Slides / Video 
4/4  Lecture 21. First Order Logics. 
Slides / Video 
4/9  Lecture 22. First Order Logics & Intro to Axiomatic Semantics. 
Slides / Video 
4/11  Lecture 23. Axiomatic Semantics. 
Slides / Video 
4/16  Lecture 24. Axiomatic Semantics. 
Slides / Video 
4/18  Lecture 25. Model Checking. 
Slides / Video 
Grade  A+  A  A  B+  B  B  C+  C  C  D  F 

Score  [95,100]  [90,94]  [85,89]  [80,84]  [75,79]  [70,74]  [65,69]  [60,64]  [55,59]  [50,54]  [0,49] 
In our commitment to academic excellence and ethical scholarship, we emphasize the importance of academic integrity in all aspects of our course. Academic integrity is central to the development of individual responsibility and scholarly credibility. Please be aware that the use of Large Language Model (LLM) tools, including ChatGPT, is strictly prohibited in the completion of any coursework and assignments in this class. These tools, while valuable in certain contexts, do not align with our commitment to original thought and individual academic effort.
As part of this course, it is essential for all students to familiarize themselves with the University of Illinois at UrbanaChampaign Student Code, which is an integral component of our syllabus. Special attention should be paid to Article 1, Part 4, which focuses on Academic Integrity. You can access and review the Student Code at http://studentcode.illinois.edu/.