Métodos Formais em Engenharia de Software

Mestrado Integrado em Engenharia Informática - MFES 2019/2020

Tópicos

Avisos

30 Mar - VF: alteração do método de avaliação. tinynew.gif

21 Fev - VF: aula de substituição será, 4ª feira, 26-Fev, às 14:00, na sala 0.04 do DI.

10 Fev - CSI: afixadas as notas finais na página de CSI.

4 Fev - As aulas de AC e VF iniciam-se esta quinta-feira, 6-Fev.

28 Jan - CSI: o exame de recurso terá lugar na sala E2-1.10 às 9h00.

26 Jan - CSI: estão lançadas as classificações após a realização do teste - ver página CSI. Atendimento para mostrar os testes: dia 27-Jan, às 16h.

13 Jan - CSI: a aula de dúvidas amanhã de tarde será às 17h, na sala 0.09, e não às 16h, como por lapso disse a alguns alunos. Pf ver Sumarios.

13 Jan - CSI: matéria para a parte 2 do teste - ver FAQ 9 na página de CSI.

13 Jan - CSI: o teste terá lugar no dia 16-Jan às 14h, na sala E7-0.07.

13 Jan - CSI: haverá uma aula de dúvidas amanhã de tarde, na sala 0.09, pf ver Sumarios.

5 Jan - EM: o prazo para a entrega do TP2 foi adiado uma semana.

2 Jan - CSI: estão lançadas as classificações do mini-teste na página CSI.

3 Dez - CSI: os alunos devem prestar atenção ao material pedagógico que vai aparecendo na página da disciplina.

24 Nov - CSI: os alunos devem prestar atenção às FAQs que vão saindo na página da disciplina.

12 Nov - CSI: mini-teste terá lugar no dia 28-Nov às 14h, na sala E7-0.07. Haverá aula depois até às 17h.

10 Nov - CSI: Caso de estudo da aula de 7-Nov ('campeonato de futebol') adicionado ao material da disciplina.

29 Out - CSI: Formulário actualizado colocado na página respectiva.

2 Out - Atenção à mudança de sala de ATS: passa para CP2.-2.08.

26 Set - Atenção à mudança de sala de CSI: passa da 1.10 para a 0.07 (Edifício 7).

17 Set - Início das aulas: 17-Set (ATS).

-- JoseNunoOliveira - 17 Sep 2019

Education » MFES » WebHome » VF

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 Sala
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.

r19 - 26 May 2020 - 09:59:59 - MariaJoaoFrade
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM