# Course
Announcement:

# EECS
498 Formal Verification Methods

# Winter 2003 -- 4 credits

Prof. Bill Rounds

rounds@umich.edu

(Upper Level Elective
for CE and Advanced Technical Elective for CS)

*How can you be sure that a hardware or software system
is really correct?*

The traditional approach to validating hardware and software
systems is to do lots of testing.
Until recently, the alternative approach of using formal methods to
prove correctness has not been practical.
One of the most important developments in this area is easy-to-use model checking
systems. In this course we will
study formal verification methods with an emphasis on model checking. You will learn to use the SMV model
checking system developed at Carnegie Mellon and use it to verify a significant
hardware or software system. This
is your chance to learn about an emerging technology! There will be three hours of lecture and an one hour of
discussion each week.

##

## Course Description

An introduction to current methodologies for verifying
computer systems. Topics covered
include logic and theorem proving; modeling sequential, reactive and concurrent
systems; transition systems; model checking methods; and controlling state
explosion. Special topics such as
temporal logic, the mu-calculus, binary decision diagrams, Buechi automata,
partial order reduction, and process algebras will be covered as time permits. Students will complete a project using
current model checking technology.

** **

**Prerequisites:** EECS
281 and EECS 376.

** **

**Course textbook: ***Logic
in Computer Science: Modelling and Reasoning about Systems*, M. Huth
and M. Ryan, Cambridge University Press, 1999. (Check Amazon for contents.)

**Course Topics**

*Week 1:* Propositional logic, natural
deduction systems, semantics and normal forms.

*Week 2:* Predicate logic and proof theory.

*Week 3:
*Semantics of predicate logic.

*Week 4:* Computation tree logic (CTL) and
the model checking algorithm.

*Week 5:* SMV model checking system; example:
checking fairness. Project
assigned.

*Week 6:
*Extensions of CTL and fixed point
characterizations.

*Week 7:
*Software verification, partial and
total correctness. Project
checkpoint.

*Week 8:
*Calculi for partial and total
correctness.

*Week 9:
*Modal logic and logic engineering.

*Week 10: *Reasoning
about knowledge in multi-agent systems.

*Week 11: *Binary decision diagrams and model checking. Project due.

*Week 12: *The satisfiability problem and model checking.

*Week 13: *Other approaches: process algebras, Buechi automata,
the mu-calculus