Formal Software Development Methods

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 bug-finding techniques for sequential and more challenging programs (e.g., concurrent, non-deterministic, 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, model-checking, and developing programs using contracts.

Please note that this is an in-person 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!

 Every Tuesday / Thursday
 12:30 PM - 01:45 PM
 Location: DCL, Room 1310
 Forum: Campuswire

 Gagandeep Singh
 Assistant Professor
 Computer Science, UIUC
 Office hour:
 Thursday 5:30pm-6:30pm (SC 4214)

 Avaljot Singh
 Computer Science, UIUC
 Office hour:
 Wednesday 3pm-4pm (SC 3102)

 Ruipeng Han
 Computer Science, UIUC
 Office hour:
 Wednesday 3pm-4pm (SC 3102)


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 grade using the following table:

Activity Grade Details
Homeworks 90 pts
  • A total of 6 homeworks. 3 homeworks before spring break, and 3 after. The lowest grade will be dropped.
Attendance 10 pts
  • Attendance will start at the 3rd week. No drops for unexcused absences.

For Graduate Students: 25 pts
  • Students in the 4-credit section need to do a course project either individually or in groups of 2.

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.

Homework Policy

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 four-day late submission allowance, any further late homework submissions will result in a penalty of 33% grade reduction / day.


Tentative Schedule  

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

Lecture 1. Course Introduction

Slides / Video

Lecture 2. Backgrounds

Slides / Video

Lecture 3. Cancelled due to Inclement Weather


Lecture 4. Backgrounds Continued & Control-Flow Graph

Slides (Same as Lecture 2) / Video

Lecture 5. Operational Semantics

Slides (Same as Lecture 2) / Video

Lecture 6. Operational Semantics Continued

Slides / Video

Lecture 7. Intro to Symbolic Execution

Slides / Video

Lecture 8. Symbolic Execution Continued

Slides / Video

Lecture 9. Static Analysis

Slides / Video

Lecture 10. Static Analysis Continued

Slides / Video

Lecture 11. Static Analysis Continued

Slides / Video

Lecture 12. Static Analysis Continued

Slides / Video

Lecture 13. Data Flow Analysis

Slides / Video

Lecture 14. Data Flow Analysis.

Slides / Video

Lecture 15. Data Flow Analysis.

Slides / Video

Lecture 16. Abstract Interpretation.

Slides / Video

Lecture 17. Abstract Interpretation.

Slides / Video

Lecture 18. Abstract Interpretation.

Slides / Video

Lecture 19. Propositional Logics.

Slides / Video

Lecture 19. First Order Logics.

Slides / Video

Lecture 20. First Order Logics.

Slides / Video

Lecture 21. First Order Logics.

Slides / Video

Lecture 22. First Order Logics & Intro to Axiomatic Semantics.

Slides / Video

Lecture 23. Axiomatic Semantics.

Slides / Video

Lecture 24. Axiomatic Semantics.

Slides / Video

Lecture 25. Model Checking.

Slides / Video

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