Verificação 22/05/2012

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

Temas de Seminário sugeridos pelo professor:
  - Unbunded model checking
  - CEGAR
  - Timed Automata
  - Reduções de Ordem Parcial
  - Spin
  - UPAAL
  - Simulação (o concorrente dos model checking)
  - Provadores de Teoremas
  - Redes de Petri

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

Outros temas discutidos na aula:

Ferramentas de Modelagem:
  - Spin   - Ferramenta de Estado Explicito.
  - UPPAAL - Concorrente do prisma

Vantagens do Spin:
  - Estado explicito
  - Não explode de repente

Ferramenta de Provador de Teoremas:
  - Twelf - máquina virtual para a linguagem elf. (citada por um aluno)

Linguagem de Algebra de Processos:
  - B
  - Z
  - CSP

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

Sugestão sobre os seminários:
  - Coloque no ultimo slide um sumário, para facilitar as discussões (como parte da conclusão).
  - Uma apresentação deve contar uma história e não listar itens.
  - O objetivo é minimizar o texto e máximizar a história da apresentação.