|
|
COMP- 525:
FORMAL VERIFICATION
|
|
Course Summary
-
Model checking is an automated technique for proving that a system
(described as a transition system) satisfies a specification written in some formal language. In this class we develop the logic background, especially temporal logic and show how model checking works. We study binary decision diagrams which have allowed industrial strength systems to be verified in practice. We end with
special topics like Buchi automata and real-time systems.
|
