CS477 - Formal Software Development Methods

Course Description

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

Instructor :

Gagandeep Singh
Tenure-Track Assistant Professor
Computer Science, UIUC
4110 Siebel Center
ggnds@illinois.edu
Office hours (TBD)

Teaching Assistants:

Avaljot Singh
avaljot2@illinois.edu
Office Hours (TBD)

Ruipeng Han
avaljot2@illinois.edu
Office Hours (TBD)

Lectures:

Tuesday/Thursday
11:00am-12:15pm
Online: Zoom link
Piazza: Code
Gradescope: Code

Assignments and Projects

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 133 points; scaled to 100%). We will compute the final grade using the following table:

Tentative Schedule

1. Background and Predicate Logic
2. Operational Program Semantics
3. Static Analysis and Abstract Interpretation
4. First Order Logic, Hoare Logic and Code Contracts
5. Model Checking
6. Advanced Topics

Latest Updates