CS 476

CS 476 - Program Verification

Fall 2024

Title	Rubric	Section	CRN	Type	Hours	Times	Days	Location	Instructor
Program Verification	CS476	D3	35855	LCD	3	0930 - 1045	T R	101 Transportation Building	Jose Meseguer
Program Verification	CS476	D4	35852	LCD	3	0930 - 1045	T R	101 Transportation Building	Jose Meseguer

See full schedule from Course Explorer

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; one of CS 374, ECE 374 or MATH 414.

Subject Area

Programming Languages / Formal Methods

Course Director

Jose Meseguer

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

Last updated

2/25/2019by Jose Meseguer