Verificação Automática: Model Checking

Professor: Sérgio Vale Aguiar Campos

• scampos@dcc.ufmg.br
• sala 4041

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
  • Original BDD paper (Bryant, 1986).
• 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.
  • Paper on partitioned transition relations.
  • Paper on compositional reasoning.
• 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: