Prof. Bill Rounds
(Upper Level Elective for CE and Advanced Technical Elective for CS)
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.
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.)
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