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.

 

News  

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


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

 Instructor:
 Gagandeep Singh
 Assistant Professor
 Computer Science, UIUC
 ggnds@illinois.edu
 Office hour:
 Thursday 5:30pm-6:30pm (SC 4214)

 TAs:
 Avaljot Singh
 Computer Science, UIUC
 avaljot2@illinois.edu
 Office hour:
 Wednesday 3pm-4pm (SC 3102)

 Ruipeng Han
 Computer Science, UIUC
 ruipeng2@illinois.edu
 Office hour:
 Wednesday 3pm-4pm (SC 3102)

Overview  

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
1/15

Lecture 1. Course Introduction


 Slides / Video
1/18

Lecture 2. Backgrounds


 Slides / Video
1/18

Lecture 3. Cancelled due to Inclement Weather
1/25

Lecture 4. Backgrounds Continued & Control-Flow Graph


 Slides (Same as Lecture 2) / Video
1/30

Lecture 5. Operational Semantics


 Slides (Same as Lecture 2) / Video
2/1

Lecture 6. Operational Semantics Continued


 Slides / Video
2/6

Lecture 7. Intro to Symbolic Execution


 Slides / Video
2/8

Lecture 8. Symbolic Execution Continued


 Slides / Video
2/13

Lecture 9. Static Analysis


 Slides / Video
2/15

Lecture 10. Static Analysis Continued


 Slides / Video
2/20

Lecture 11. Static Analysis Continued


 Slides / Video
2/22

Lecture 12. Static Analysis Continued


 Slides / Video
2/27

Lecture 13. Data Flow Analysis


 Slides / Video
2/29

Lecture 14. Data Flow Analysis.


 Slides / Video
3/5

Lecture 15. Data Flow Analysis.


 Slides / Video
3/7

Lecture 16. Abstract Interpretation.


 Slides / Video
3/19

Lecture 17. Abstract Interpretation.


 Slides / Video
3/21

Lecture 18. Abstract Interpretation.


 Slides / Video
3/26

Lecture 19. Propositional Logics.


 Slides / Video
3/28

Lecture 19. First Order Logics.


 Slides / Video
4/2

Lecture 20. First Order Logics.


 Slides / Video
4/4

Lecture 21. First Order Logics.


 Slides / Video
4/9

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


 Slides / Video
4/11

Lecture 23. Axiomatic Semantics.


 Slides / Video
4/16

Lecture 24. Axiomatic Semantics.


 Slides / Video
4/18

Lecture 25. Model Checking.


 Slides / Video
4/23

Lecture 26. Guest Lecture 1 (Termination Analysis).


 Slides / Video
4/25

Lecture 27. Guest Lecture 2 (Syncode).


 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 http://studentcode.illinois.edu/.