Pós-Grad: Aula com professor da UFMG

Postado por: Marcos

Nos dias 22-23/6 e 6-7/7, a Facom receberá o professor Sergio Campos (http://homepages.dcc.ufmg.br/~scampos/) para ministrar a disciplina Verificação Automática. A aula é aberta a todos os interessados. Confira, abaixo, uma descrição da área de pesquisa.


Verificação Automática – Model Checking

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.