CS 477

CS 477 - Formal Software Devel Methods

Fall 2026

Title	Rubric	Section	CRN	Type	Hours	Times	Days	Location	Instructor
Formal Software Devel Methods	CS477	B3	64565	LCD	3	1100 - 1215	T R	3018 Campus Instructional Facility	Madhusudan Parthasarathy
Formal Software Devel Methods	CS477	B4	64566	LCD	4	1100 - 1215	T R	3018 Campus Instructional Facility	Madhusudan Parthasarathy
Formal Software Devel Methods	ECE478	B3	66706	LCD	3	1100 - 1215	T R		Madhusudan Parthasarathy
Formal Software Devel Methods	ECE478	B4	66707	LCD	4	1100 - 1215	T R		Madhusudan Parthasarathy

See full schedule from Course Explorer

Web Page

https://courses.engr.illinois.edu/cs477/fa2021/

Official Description

Mathematical models, languages, and methods for software specification, development, and verification. Course Information: Same as ECE 478. 3 undergraduate hours. 3 or 4 graduate hours. Prerequisite: CS 225; one of CS 374, ECE 374 or MATH 414.

Course Director

Madhusudan Parthasarathy

Text(s)

Varies by semester.

Learning Goals

Be able to do solve problems using structural induction (1,6)

Write code contracts, invariants, and assertions that describe a program's specification formally. (3, 5, 6)

Analyze a program with assertions and find inductive invariants to prove the program correct (1,2, 6)

Given a program with assertions and inductive invariants, be able to derive verification conditions in logic. (1,2,6)

Be able to formulate specifications and properties of structures in logic. (1,2)

Give proofs in Hoare Logic of properties about simple imperative programs. (1,2,6)

Build an abstract interpretation scheme for a program that is sound with respect to given desired properties. (1,2,6)

Topic List

Formal Logics
Hoare Logic
Abstract Interpretation

Required, Elective, or Selected Elective

Selected Elective.

Last updated

2/14/2019by Madhusudan Parthasarathy