Graduate course at DCC/UFMG
Model checking is a technique for verifying finite-state concurrent systems such as sequential circuit designs and communication protocols. It has a number of advantages over traditional approaches that are based on simulation, testing and deductive reasoning. In particular, model checking is automatic and usually quite fast. Also, if the design contains an eror, model checking will produce a counterexample that can be used to pinpoint the source of the error. The method has been used successfully in practice to verify real industrial designs, and several companies are beginning to market commercial model checkers. Among its many academic accomplishments we should mention an ACM Doctoral Dissertation Award for Ken McMillan in 1992, the ACM Paris Kanellakis Award for Theory and Practice in 1999 and the recent Turing Award for Amir Pnueli, for his work on verification based on temporal logic, the basis for model checking.
The course will discuss verification in general, the basics of model checking and several advanced topics, required for practical uses of the method.
Notas finais lancadas em 12/07/2010
Observacoes: 30%, trabalho 1, 10% apresentacao, 60% trabalho final
Marcelo, Fernando, Rogerio, Alison, nao tenho o TP1 de voces, me procurem.