Verificação Formal

Docentes: Jorge Sousa Pinto e Maria João Frade

Slides

• Apresentação
• Propositional Logic and SAT solvers
• First-Order Logic and SMT
• SMT solvers
• Logic and Type Theory
• The Coq Proof Assistant: part1, part2, part3

Exemplos e Exercícios

• SAT
  • Exemplos
• SMT
  • Exemplos
• Coq
  • Ficheiros para as aulas
  • Ficha de exercícios

Ferramentas

• SAT Live! - keep up to date with research on the satisfiability problem
• SMT-LIB - The Satisfiability Modulo Theories Library
• Frama-C - Software Analyzers
• CBMC - A Bounded Model Checker for C and C++ programs.
• The Coq Proof Assistant

• Máquina virtual com todas as ferramentas instaladas: Xubuntu-64bit.ova README

Código

• pasta Dropbox partilhada

Alguns links e notícias sobre VF

Provas de Avaliação

• Projecto.
• Avaliação laboratorial sobre Frama-C e CBMC: 27 de Abril.
• Avaliação laboratorial sobre Coq: 1 Junho.