skip to main content

Course Websites

CS 476 - Program Verification

Spring 2021

Official Description

Formal methods for demonstrating correctness and other properties of programs. Invariant assertions; Hoare axiomatics; well-founded orderings for proving termination; structural induction; computational induction; data structures; parallel programs; overview of predicate calculus. Course Information: 3 undergraduate hours. 3 or 4 graduate hours. Prerequisite: CS 225; CS 374 or MATH 414.

Related Faculty

Subject Area

Programming Languages / Formal Methods

Course Director

Text(s)

M. Clavel et al., All About Maude, Springer LNCS 4350, 2007

P.C. Olveczky, Designing Reliable Distributed Systems, Springer, 2017

Learning Goals

Be able to model software systems mathematically using mathematical logic. (1) (2) (3) (4) (6)

Be able to model mathematically the semantics of programs and to use such a semantics to verify program properties. (1) (2) (3) (4) (6)

Be able to fornally verify both sequential and concurrent programs in both declarative and imperative languages. (1) (2) (3) (4) (5) (6)

Be able to to develop correct formal executable specifications of software systems, and to use such specifications to verify system properties. (1) (2) (3) (4) (5) (6)

Be able to correctly use the main logics involved in the verification of both sequential and concurrent programs and systems, including, equational logic, rewriting logic, inductive first-order loic, Hoare logic, and temporal logic. (1) (2) (3) (5) (6)

Be able to effectively and competently use formal verification tools such as formal specification languages, theorem provers, and model checkers to verify programs and systems using all the above-mentioned logics in non-trivial practical examples. (1) (2) (3) (4) (5) (6)

Topic List

Algebraic specification of declarative sequantial programs

Inductive first-order logic and inductive theorem proving

Formal verification of declarative functional programs

Algebraic semantics of imperative sequential languages

Hoare logic and formal verification of imperative sequential programs

Rewriting logic specification of declarative concurrent programs

Temporal logic and model checking verification of declarative concurrent programs

Rewriting logic semantics of imperative concurrent programs

Model checking verification of imperative concurrent programs

Reachability logic verification of imperative and declarative concurrent programs

Assessment and Revisions

Revisions in last 6 years Approximately when revision was done Reason for revision Data or documentation available?

The lecture notes have been improved each year based on feedback from the students. The main goal has been to find simpler ways to expain the material. Also, since the familiarity with basic set theory concepts of many students was in fact quite tenuous, supplementary notes on set theory which are properly not part of the course but do help the students follow set-theoretic notation and master the mathematical logic used in the course have also been developed and have been made available to the students.

Eac year

Making the material more accessible, and helping the

lack of mathematical maturity of most students, as

already explained.

Yearly lecture notes are available.

Required, Elective, or Selected Elective

Elective

TitleSectionCRNTypeHoursTimesDaysLocationInstructor
Program VerificationD339586ONL30930 - 1045 T R    Jose Meseguer
Program VerificationD439587ONL40930 - 1045 T R    Jose Meseguer