Verificação Formal

Docente: Maria João Frade

Slides

• Apresentação
• Propositional Logic and SAT solvers
• First-Order Logic and SMT
• SMT solvers
• Semantics: slides1, slides2, slides3, slides4
• Deductive Program Verification
• Deductive Program Verification with Frama-C: part1, part2
• Bounded Model Checking of SW: Introduction to CBMC, CBMC by Example
• Logic and Type Theory
• The Coq Proof Assistant: part1, part2, part3

Exemplos

• SAT
  • The unicorn puzzle

• SMT
  • Scheduling problem
  • Modeling assignments and array updates

• Frama-C
  • Ficheiros para as aulas
  • Alguma documentação

• CBMC
  • Ficheiros para as aulas
  • Alguma documentação

• Coq
  • Ficheiros para as aulas
  • Alguma documentação
  • Ficha de exercícios

Ferramentas

• SATLIB - The Satisfiability Library
• 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

Provas de Avaliação

• Enunciado do projecto (SMT solvers) (Entrega: 26 de Abril) -- Notas
• Avaliação laboratorial sobre Frama-C e CBMC: 7 de Maio. -- Notas
• Avaliação laboratorial sobre Coq: 18 Junho. -- Notas

Notas Finais

• Época Normal
• Recurso