CS 356: Automatic Formal Verification Techniques

Spring Quarter 2003-2004

Course Description

This class covers theoretical and practical aspects of computer-assisted formal verification of systems. Emphasis will be on the more practical and more automatic methods, especial model checking for finite-state system.

Lectures

Lectures are held every Monday and Wednesday in Gates 100 from 9:30-10:45 AM except University holidays.

The course will be taught by Prof. David Dill.

Handouts

Handouts, including lecture notes, will generally be available on the web.

Assignments

There will be more-or-less biweekly homeworks, which will be a combination of programming, use of verification tools, and written problems. Homeworks will generally be assigned each Wednesday and due a week later.

Credit and Grading

Grades will be based on homeworks, the project, and class participation. There will be no exams.

Questions & Mailing Lists

Send questions (also regarding assignments) to "cs356@verify.stanford.edu".

If everything else fails, questions can be directed to David Dill (dill@cs.stanford.edu).

Tentative Schedule (this is in a state of flux, so don't rely too much on this version, except that the topics are approximately right).


Lecture	Date	Topic	Assignment
1	3/31/2004	Introduction, Murphi basics.
2	4/5/2004	Murphi algorithms, symmetry reduction.	Give Murphi a try
3	4/7/2004	Symmetry Reduction	Hw#1, due 4/14/2004
4	4/12/2004	Probabilistic verification.
5	4/14/2004	Partial Order Reduction
6	4/19/2004	BDD basics.
7	4/21/2004	Reachability with BDDs.	HW 1 Due. hw#2, due 4/28/2004
8	4/26/2004	Reachability with BDDs.
9	4/28/2004	BDDs and FSM reachability.
10	5/3/2004	CTL model checking.	HW 2 Due. hw#3, due 5/10/2004
11	5/5/2004	More CTL model checking (fairness constraints)
12	5/10/2004	Symbolic model checking with fairness constraints.
13	5/12/2004	Verification and Formal Languages.	HW 4, due 5/24
14	5/17/2004	Omega automata
15	5/19/2004	Omega automata
16	5/24/2004	Abstraction & refinement	HW 4 Due. hw#5, due 6/2/2004
17	5/26/2004	Cooperating Decision procedures
18	6/2/2004	Predicate Abstraction

Copyright © by David L. Dill, 1998, 1999, 2000, 2001, 2002, 2003, 2004. All rights reserved. This material may be freely distributed for educational purposes, so long as (1) this copyright notice remains, (2) modifications and additional material are clearly marked so as to be distinguished from the original material, and (3) no fee is charged. Other uses require the express written consent of the authors. There are probably errors. Use at your own risk.