Spring 2006
CS 498: Software Model-Checking
2:00-3:15 Wed and Fri
1131 Siebel Ctr.

Verified software is one of the grand challenges of computer science. As the complexity of software increases and as systems pervade our day-to-day activities, verification of systems ranging from cell phones to medical equipment to aircraft software to secure programs, has become a vibrant and important field.

We will study various approaches to analyse and verify software, with emphasis on automatic techniques. We will entirely avoid techniques where substantial human help is required (such as manual theorem proving).

The course will concentrate on mainly three verification paradigms:
(a) dataflow analysis techniques (fast, scalable, but coarse analysis)
(b) explicit software verification techniques (eg. SPIN, JPF) and
(c) techniques where the system is abstracted into a tractable model which is then algorithmically/symbolically verified (eg. SLAM).
We will also discuss various specification languages that can formally describe properties of software and decision procedures to verify them.

Specific topics will include: dataflow analysis, flow sensitive/insensitive analysis, control-flow abstraction, abstract interpretation, predicate abstraction using theorem proving, finite and pushdown models, state-space exploration, symbolic techniques, abstraction refinement, abstraction of data structures and shape analysis, symbolic evaluation, reactive systems, and analysis of concurrent software. Basis of tools such as SMV, SPIN, SLAM, Bandera, Java Path Finder, Zing and TVLA will be covered.
[ This course will have little overlap with CS 476 (Software verification) and CS 477 (Formal Software Dev Methods). ]
This course requires mathematical maturity, and some knowledge of automata theory (CS 273) and basic propositional logic.

See here for a similar course offered in Spring last year and an overview of its content.