CS 477 - Formal Software Development Methods (Fall 2026)

Lecture Schedule

Prerequisite Resources

Preliminary Material
Preliminary logic primer, P. Madhusudan (for CS173)
Notes on induction on natural numbers, P. Madhusudan (for CS173)
More notes on induction, Chandra Chekuri (for CS173)

Introduction and Motivation

August 25
[Intro Slides]

Motivation and Introduction to the course, course logistics, topic covered in the the course, formal methods in the AI era.

August 27
Prop Logic

Propositional logic; satisfiability and validity, NP-completeness of SAT, deductive proof systems for propositional logic, soundness and completeness

LCS (Logic in CS notes, see resources page for link); Chapter 1; proof systems on slides only

September 1

Propositional logic contd: How SAT solvers work, the Z3/CVC SAT format. While programs: Syntax and Semantics using transition systems. Recursive functions and how they are well-defined when they induct on a well-founded order, and are computable as well.

September 3

Program Semantics. The While Programming Language. Semantics using Transition Systems. Hoare triples as the program verification problem. Operational semantics using proof systems as well.

Reference: Short Notes on Program Verification

September 8

S

September 10

Bounded Model-checking in industry to find errors; CBMC and its uses in industry (AWS Datacenters, other applications); Concolic testing and the SAGE tool at Microsoft

Introduction to Inductive Invariant based verification of systems.

September 15

First-order logic and quantifier-free logics; FO theories; SMT solvers; decidable and undecidable theories

References: Satisfiability Modulo Theories by Barrett/Tinelli; Z3 Tutorial

Resource references:

See Resource page for links to resources.
[LCS] - Logic in Computer Science, by P. Madhusudan and Mahesh Viswanathan