SPRING 2025 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 techniques for sequential and more challenging programs (e.g., concurrent, non-deterministic, probabilistic, and neuro-symbolic). 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.
Please note that this is an in-person class. The lecture details will be communicated soon. Attendance is mandatory. If you're unable to attend a class, please notify the instructor with a valid reason.
02/14/2025: Homework 2 released. NOTE: Two separate submissions are required - one each for the theory and the programming problems
01/23/2025: Campuswire, course website link is sent by email.
01/21/2025: The website is up!
We will inform you about the grading policy at the beginning of the class.
Date | Topic | Notes | Related readings |
---|---|---|---|
01/21 | Lecture 1. Course Introduction |
Slides | |
01/23; 01/28; 01/30; | Lecture 2,3,4. Background; CFGs; Big Step Semantics |
Slides | |
02/04 | Lecture 5. Small Step Semantics |
Slides | |
02/06 | Lecture 6. Propositional Logic |
Slides | |
02/11, 2/13 | Lecture 7, 8. Symbolic Execution |
Slides |
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, unless explicitly specified otherwise. 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 Urbana-Champaign 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/.