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

Docente Horário Salaup
Maria João Frade 5a-feira, 14h-17h Sala E7 0.07
Jorge Sousa Pinto 5a-feira, 14h-17h Sala E7 0.07

Alunos

# Nome Curso
a82441 Alexandre Mendonça Pinho MIEI
a80453 Bárbara Andreia Cardoso Ferreira MIEI
pg40866 Bruno Manuel Pereira Antunes MMC
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
pg41094 Pedro Rafael Paiva Moura MEI
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

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.