CS 477
CS 477 - Formal Software Devel Methods
Spring 2025
| Title | Rubric | Section | CRN | Type | Hours | Times | Days | Location | Instructor |
|---|---|---|---|---|---|---|---|---|---|
| Formal Software Devel Methods | CS477 | B3 | 39588 | LCD | 3 | 1230 - 1345 | T R | 1310 Digital Computer Laboratory | Gagandeep Singh |
| Formal Software Devel Methods | CS477 | B4 | 39589 | LCD | 3 | 1230 - 1345 | T R | 1310 Digital Computer Laboratory | Gagandeep Singh |
| Formal Software Devel Methods | ECE478 | B3 | 39766 | LCD | 3 | 1230 - 1345 | T R | 1310 Digital Computer Laboratory | Gagandeep Singh |
| Formal Software Devel Methods | ECE478 | B4 | 39767 | LCD | 3 | 1230 - 1345 | T R | 1310 Digital Computer Laboratory | Gagandeep Singh |
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
Assessment and Revisions
| Revisions in last 6 years | Approximately when revision was done | Reason for revision |
| Each semester the instructor has chosen difference emphases in order to introduce and interest the students in recent research topics. | This helos to serve learning outcome (h) recognition of the need for and an ability to engage in continuing professional development |
Required, Elective, or Selected Elective
Selected Elective.