Course Websites

CS 477 - Formal Software Devel Methods

Last offered Spring 2024

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.

Related Faculty


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.

Formal Software Devel MethodsB339588LCD31230 - 1345 T R  1310 Digital Computer Laboratory Gagandeep Singh
Formal Software Devel MethodsB439589LCD31230 - 1345 T R  1310 Digital Computer Laboratory Gagandeep Singh