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
TA:
Shaurya Gomber
2nd year PhD Student
Computer Science, UIUC
sgomber2@illinois.edu
Office hour: Friday 4pm - 5pm
Location: SC 2303
Overview
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
We will inform you about the grading policy at the beginning of the class and update here soon.
Tentative Schedule
| Date | Topic | Slides / Video |
|---|---|---|
| 01/20 | Lecture 1. Course Introduction | Slides | Video |
| 01/22 | Lecture 2. Background | Slides | Video |
| 01/27 | Lecture 3. CFGs | Slides (same as 01/22) |
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] |
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 http://studentcode.illinois.edu/.