CS 477 - Formal Software Devel Methods

Fall 2021

Formal Software Devel MethodsCS477B364565ONL31100 - 1215 T R    Sasa Misailovic
Formal Software Devel MethodsCS477B464566ONL41100 - 1215 T R    Sasa Misailovic
Formal Software Devel MethodsECE478B366706ONL31100 - 1215 T R    Sasa Misailovic
Formal Software Devel MethodsECE478B466707ONL41100 - 1215 T R    Sasa Misailovic

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; CS 374 or MATH 414.


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.

Last updated

2/14/2019by Madhusudan Parthasarathy