Formal Software Development Methods

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.

 

News  

  • 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!


 Lectures:
 Every Tuesday / Thursday
 12:30 PM - 1:45 PM
 Location: 1310 Digital Computer Laboratory
 Forum: Campuswire

 Instructor:
 Gagandeep Singh
 Assistant Professor
 Computer Science, UIUC
 ggnds@illinois.edu
 Office hour: Tuesday 3pm - 4pm.
 Location: SC 4214

 TA:
 Debangshu Banerjee
 Computer Science, UIUC
 db21@illinois.edu
 Office hour: Wednesday 4:30 pm - 5:30 pm.
 Location: SC 3401

 TA:
 Hrishikesh Balakrishnan
 Computer Science, UIUC
 hb19@illinois.edu
 Office hour: Wednesday 4:30 pm - 5:30 pm.
 Location: SC 3401

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.

Grading Policy

We will inform you about the grading policy at the beginning of the class.

 

Tentative Schedule  


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
 

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/.