Formal Verification

Course information

Formal Verification
Instructor: Dr. Bijan Alizadeh
Spring 2008

Content

COURSE OBJECTIVES

Why and Where Formal Verification
How to formally verify digital systems
Formal Verification Algorithms
Formal Verification concepts

TEXT BOOK

E.M. Clarke, O. Grumberg, D. Peled: Model Checking, MIT Press, 2000.
T. Kropf. Introduction to Formal Hardware Verification, Springer Verlag, 1999.
T.F. Melham: Higher Order Logic and Hardware Verification, Cambridge Tracts in Theoretical Computer Science, No 31, Cambridge University Press, 1993.
Lecture notes.
Selected papers.

COURSE OUTLINES

1. Why and Where Formal Verification (PDF)

n2. General overview of Formal Verification Methods

n3. Introduction to property languages (PDF)

n LTL

n CTL

n PSL

n4. Introduction to decision diagrams

n Bit level DDs (PDF)

n Word level DDs (PDF)

n5. Formal Methods

n6. Equivalence Checking methods and algorithms (PDF)

n Combinational E.C.

n Sequential E.C.

n Introduction to VIS

n7. Property checking methods and algorithms (PDF)

n Model checking

n Symbolic model checking

n Introduction to VIS (PDF)

n Advanced topics

8. Theorem proving approach (PDF)

n Introduction to higher order logic

n HOL package

n9. Introduction to decision procedures

n Satisfiability problems (PDF)

n SAT solvers

n SMT solvers

n10. Introduction to symbolic simulation (PDF)

n11. Assertion-based verification

n12. High level formal verification approaches (PDF, PDF)

n13. Hybrid verification methods

Grading

Computer Assignments 20%
Presentation 20%
Project 25%
Final Exam 35%

Additional Documents

Assignments

HOMEWORKS

Useful links

Course information	Formal Verification Instructor: Dr. Bijan Alizadeh Spring 2008
Content	COURSE OBJECTIVES Why and Where Formal Verification How to formally verify digital systems Formal Verification Algorithms Formal Verification concepts TEXT BOOK E.M. Clarke, O. Grumberg, D. Peled: Model Checking, MIT Press, 2000. T. Kropf. Introduction to Formal Hardware Verification, Springer Verlag, 1999. T.F. Melham: Higher Order Logic and Hardware Verification, Cambridge Tracts in Theoretical Computer Science, No 31, Cambridge University Press, 1993. Lecture notes. Selected papers. 1. 2. 2. COURSE OUTLINES 1. Why and Where Formal Verification (PDF) n n2. General overview of Formal Verification Methods n n3. Introduction to property languages (PDF) n LTL n CTL n PSL n4. Introduction to decision diagrams n Bit level DDs (PDF) n Word level DDs (PDF) n5. Formal Methods n n6. Equivalence Checking methods and algorithms (PDF) n Combinational E.C. n Sequential E.C. n Introduction to VIS n n7. Property checking methods and algorithms (PDF) n Model checking n Symbolic model checking n Introduction to VIS (PDF) n Advanced topics 8. Theorem proving approach (PDF) n Introduction to higher order logic n HOL package n n9. Introduction to decision procedures n Satisfiability problems (PDF) n SAT solvers n SMT solvers n n10. Introduction to symbolic simulation (PDF) n n11. Assertion-based verification n n12. High level formal verification approaches (PDF, PDF) n n13. Hybrid verification methods
Grading	Computer Assignments 20% Presentation 20% Project 25% Final Exam 35%
Additional Documents
Assignments	HOMEWORKS
Useful links