UC3 - Verificação Formal
Programa Resumido
- Lógica e Sistemas de Prova
- Sistemas de prova automática:
- lógica proposicional; SAT solvers;
- lógica de 1ª ordem; teorias de 1ª ordem; SMT solvers.
- Sistemas de prova assistida:
- lógica de ordem superior; the Coq proof assistant.
- Verificação de Software
- Verificação dedutiva de programas:
- lógica de Hoare; VCGen; safety verification; functional verification;
- a plataforma Why3 para verificação dedutiva de programas;
- anotações em ACSL; o plug-in WP da ferramenta Frama-C.
- Verificação automática de programas:
- bounded model checking of software; CBMC.
Material de Apoio
Slides
Guiões
Ferramentas
Uma parte substancial do software listado é desenvolvido em Ocaml, uma linguagem funcional da família ML, e pode ser compilado localmente. Recomenda-se a instalação do package manager
OPAM (disponível em
Homebrew para Max OSX).
Máquina virtual com todas as ferramentas instaladas.
Bibliografia
- Logic in Computer Science: Modelling and Reasoning About Systems. Michael Huth & Mark Ryan. Cambridge University Press; 2nd edition (2004).
- The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley & Zohar Manna. Springer (2007).
- Rigorous Software Development: An Introduction to Program Verification. J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Springer (2011)
- Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Yves Bertot & Pierre Casteran. Springer (2004)
Funcionamento
Avaliação
-
2 testes, com nota mínima (agregada) de 8 valores (70%)
-
1 trabalho desenvolvido em grupo, envolvendo o estudo de um tópico (diferente para cada grupo), e possivelmente algum desenvolvimento. O trabalho deverá dar origem a um artigo a entregar no final do semestre, bem como a uma apresentação feita por todo o grupo (30%)
Dadas as circunstâncias muito particulares de funcionamento desta UC este ano lectivo, o método de avaliação foi alterado.
A avaliação será feita com base nos seguintes elementos:
- 2 ou 3 exercícios a serem resolvidos em casa semanalmente (e entregues por e-mail) para cada uma das duas partes do curso. Esta componente de avaliação dará origem a uma nota final de, no máximo, 15 valores.
- um trabalho final opcional, envolvendo uma ou mais ferramentas estudadas no curso, para estudantes que desejam ter uma nota final superior a 15.
Docente / Horário
Alunos
| # | Nome | Curso |
|---|
| pg41094 | Pedro Rafael Paiva Moura | MEI |
| a82441 | Alexandre Mendonça Pinho | MIEI |
| a80453 | Bárbara Andreia Cardoso Ferreira | MIEI |
| a80564 | Carla Isabel Novais da Cruz | MIEI |
| a83344 | Eduardo Jorge Lima Pinto Barbosa | MIEI |
| a78073 | João Costeira Faria Gomes | MIEI |
| a80397 | João Nuno Alves Lopes | MIEI |
| a82885 | José Augusto Ferreira Alves | MIEI |
| a68547 | Lucas Ribeiro Pereira | MIEI |
| a74036 | Manuel João Curopos Monteiro | MIEI |
| a82400 | Márcio Alexandre Mota Sousa | MIEI |
| a82535 | Pedro Mendes Pinto | MIEI |
| a82313 | Pedro Teixeira Gonçalves | MIEI |
| a75411 | Ricardo Guerra Leal | MIEI |
| a73577 | Ricardo Ribeiro Pereira | MIEI |
| a82572 | Sara Maria Barreira Melo | MIEI |
| a75328 | Tiago João Fernandes Baptista | MIEI |
| pg40866 | Bruno Manuel Pereira Antunes | MMC |
Projecto Opcional
Este
projecto opcional poderá ser desenvolvido em duas modalidades:
- individualmente, em Why3 ou em Coq;
- em grupos de dois, neste caso, em Why3 e em Coq.
O projecto deverá ser entregue até ao dia
15 de Julho.
screencast videos disponíveis no Blackboard)