Verificação Automática: Model Checking

Professor: Sérgio Vale Aguiar Campos

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.


Additional Resources:

  • Petri Nets examples and tutorials