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