CS 477
CS 477 - Formal Software Devel Methods
Fall 2025
| Title | Rubric | Section | CRN | Type | Hours | Times | Days | Location | Instructor |
|---|---|---|---|---|---|---|---|---|---|
| Formal Software Devel Methods | CS477 | B3 | 64565 | ONL | 3 | 1100 - 1215 | T R | Sasa Misailovic | |
| Formal Software Devel Methods | CS477 | B4 | 64566 | ONL | 4 | 1100 - 1215 | T R | Sasa Misailovic |
See full schedule from Course Explorer
Official Description
Course Director
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.