Date | Topic | Papers | Presenter |
---|---|---|---|
1/18 | Intro to Verification; SMV | ||
1/25 | CTL Model Checking; SMV |
|
|
2/1 | LTL Model Checking | Model Checking Using Automata Theory (by Peled), sections 1-4,6. | Peter Gilbert |
2/8 | CTL versus LTL Model Checking | Branching versus Linear Time: Final Showdown (by Vardi) | Kathi |
2/15 | BDDs and Symbolic Model Checking |
|
|
2/22 | Abstraction and Minimization |
| |
3/1 | Compositional Reasoning and Symmetry | ||
3/8 | Introduction to ACL2 | ||
3/15 | Theorem Proving and ACL2 | ||
3/22 | Abstraction in Theorem Proving | ||
3/29 | Symbolic Simulation | Symbolic Simulation: An ACL2 Approach (by Moore) | |
4/5 | No class | ||
4/12 | Case Study: The Pentium Bug |
|
|
4/19 | Verification in Practice Project Presentations |
| |
4/26 | Project Presentations |
Links to
Survey Articles on Formal Verification
Gupta's article is particularly good. The introductory "big picture" section is definitely worth reading.
A site about UCITA, the Uniform Computer Information Transactions Act.
This page maintained by Kathi Fisler Department of Computer Science Worcester Polytechnic Institute |