This course is dedicated to the study of formal techniques for building reliable software systems, covering both classical software components as well as systems that incorporate machine learning models. The course begins by introducing the mathematical foundations for formally representing software as mathematical objects and for reducing verification problems to mathematical theorems. Building on this foundation, we introduce key abstractions, such as contract-based programming, that enable precise specification of software behavior and support modular, scalable, and reliable system development.
We will study a range of verification and bug-finding techniques applicable to both traditional software systems and more challenging settings, including concurrent, non-deterministic, probabilistic, and neuro-symbolic systems. The course will combine theory and practice: students will gain hands-on experience with tools that verify important system properties such as safety, correctness, and termination using abstraction-based techniques, model checking, and contract-driven development.
The lectures can be attended in person (DCL, Room 1310) and online on Zoom. Lectures will be held on Tuesdays and Thursdays, 12:30–1:45 PM. The lecture details will be communicated soon.
News 
01/19/2026: Campuswire, course website link is sent by email.
01/19/2026: The website is up!
Every Tuesday / Thursday
12:30 PM - 1:45 PM
Location: 1310 Digital Computer Laboratory
Zoom: Link
Forum: Campuswire
Instructor:
Gagandeep Singh
Assistant Professor
Computer Science, UIUC
ggnds@illinois.edu
Office hours: Tuesday 2pm - 3pm
Location: SC 4214
TAs:
Shaurya Gomber
2nd year PhD Student
Computer Science, UIUC
sgomber2@illinois.edu
Office hour: Friday 4pm - 5pm
Location: SC 2303
Logistics
Prerequisites:
Students should have taken CS173 (or a similar course) and know basic proofs using induction and proof by contradiction (as taught in CS173).
Some background on computability theory (as taught is CS374) would be good. Prior exposure to Programming Languages and Compilers (CS421) will be
helpful but is not strictly required.
Grading Policy:
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 125 points; scaled to 100%). We will compute the final points using the following table:
| Activity | Grade | Details |
|---|---|---|
| Homeworks | 100 pts | A total of 6 homeworks. 3 before spring break and 3 after. The lowest grade will be dropped (best 5 considered). |
| For Graduate Students | 25 pts | Students in the 4-credit section must complete a course project individually or in groups of 2. |
We will use Gradescope for homework submissions and Campuswire for course announcements and discussions. Email the TA for the access codes for Gradescope and Campuswire.
Tentative Grading Scale:
| 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] |
Late Submission Policy:
You can use up to 4 extra days across all homeworks for late submissions.
- If you submit 5 minutes late, it will count as 1 extra day.
- If you use all extra days, then any further late submission will cause a 25% grade reduction per day.
Lecture Schedule
| Date | Topic | Slides / Video |
|---|---|---|
| 01/20 | Lecture 1: Introduction | Slides | Video |
| 01/22 | Lecture 2: Background | Slides | Video |
| 01/27 | Lecture 3: CFGs, Big Step Semantics | Slides (Same as 01/22) | Video |
| 01/29 | Lecture 4: Small Step Semantics | Slides | Video |
Academic Integrity
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 https://studentcode.illinois.edu/.