Verificação 03/04/2012

   # # # # # # # # # # # # #
  # Verificação Automatica  #
  # Prof. Sérgio Campos     #
  # notasdogarcia.blog.com  #
   # # # # # # # # # # # # #

  Hoje a aula começou com o Fernando, ex-aluno do Sérgio
  falando sobre o projeto de criação de um model checker.

  Este model checker pode ser nosso projeto de fim de semestre, ou seja termina-lo.

 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

  Usa-se um subconjunto do SMV, ou seja é bastante simples.

  O projeto usa um sistema de BDDs, o que é interessante.

  O nosso trabalho seria terminar algunas funções como o NEXT

  E fazer o mapeamento das formulas para SAT.

 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

  Tarefas:

    - Helper é uma interface, com logs display de erros e ferramentas do genero.
    - Optimizer, heuristicas e etc.
    -

  Outro tópico: quando vale a pena usar aproximação de model checking e o model checking própriamente dito por assim dizer.

 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

  SAT

  SAT é um modelo de checagem muito eficiente. e ele resolve o problema de: Será que esse problema logico tem solução alcansável?
  Ele resolve um problema de checagem de complexidade NP-Completo de forma heuristica obviamente.

  O SAT já existe a dificuldade em seu uso é a codificação de um problema para se adequar a sua entrada.

 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

  [email protected]

  Site com o código do Checker:
  http://code.google.com/p/ismc/wiki/Gramatica

  Mande emails com o assunto:
  VA 2012

  // Fim da aula