# 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.

#### Classes:

- Class 1: General info and a bit of history. PDF
- Class 2: Reactive Systemas and Temporal Properties. PDF
- Class 3: Model Checking Overview. PDF
- Class 4: Temporal Logic Model Checking. PDF
- Class 5: Binary Decision Diagrams. PDF
- Class 4 (): Basic fixpoint theorems.
- Class 5 (): Symbolic model checking. PDF.
- Class 6 (): Symbolic model checking (cont).
- Class 7 (): SMV. PDF.
- Class 8 (): SMV (cont).
- Class 9 (): Compiling source code to graphs. PDF.
- Class 10 (): Verification of Real Time Systems. PDF.
- Class 11 (): Verus (cont).
- Class 12 (): LTL model checking. PDF.
- Class 13 ():
- Class 14 (): Compositional reasoning. PDF.
- Class 15 (): Compositional reasoning (cont).
- Class 16 (): Compositional reasoning (cont).
- Class 17 (): SAT Solvers PDF.
- Class 18 (): Bounded model checking. PDF.
- Class 19 (): Symbolic trajectory evaluation PDF.
- Class 20 (): Scheduling problems using SMC.
- Class 21 (): Real-time systems.

Additional Resources:

Petri Nets examples and tutorials