Verificação Formal

2020/21

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

• Introduction
• Propositional Logic & SAT solvers
• First-Order Logic & Theories
• SMT solvers
• Deductive Program Verification with Why3 (J.-C. Filliâtre)
• Why3 labs
• Frama-C/WP-Safety
• Frama-C/WP-Functional
• Deductive Reasoning & the Coq Proof Assistant
• Inductive Reasoning in Coq
• Programming and Proving in Coq

Guiões

• SAT solving - Ficheiros para a aula
• SMT solving - Ficheiros para a aula
• Z3Py introduction: jupyter notebook, pdf, python
  • Sudoku: jupyter notebook, python
  • Skyscrapers: jupyter notebook, python
• Why3 files
• ACSL files
• Coq(1) - Ficheiros para a aula
• Coq(2) - Ficheiros para a aula
• Coq(3) - Ficheiros para a aula

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

• SAT Live! - keep up to date with research on the satisfiability problem
  • List of SAT solvers
  • Recomendado instalar: MiniSat (disponível em Homebrew para Max OSX)
  • MiniSat user guide
• SMT-LIB - The Satisfiability Modulo Theories Library
  • Solvers recomendados:
    • Z3 (disponível no Homebrew para Max OSX)
    • CVC4 (disponível Cask no Homebrew para Max OSX)
    • Yices2 (disponível no Homebrew para Max OSX)
    • Alt-ergo (disponível no Opam)
  • Documentação
  • Caso queira, pode instalar a versão pré-compilada do Z3 com suporte para Python. Pode ainda instalar o Python e o Jupyter via a distribuição Anaconda.
• The Coq Proof Assistant (disponível no Opam)
  • Recomendado instalar: CoqIde (disponível no Opam)
  • Documentação
• Why3: Where Programs Meet Provers (disponível no Opam)
  • Versão online
  • Documentação
• Frama-C - Software Analyzers (disponível no Opam)
  • Documentação
  • Wiki
  • Em particular:
    • ACSL by example
    • ACSL tutorial
    • ACSL reference manual
• CBMC - A Bounded Model Checker for C and C++ programs.

Máquina virtual com todas as ferramentas instaladas.

• Software instalado
• Instalação de ferramentas do Frama-C (Switch Opam)

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

Método de Avaliação

A avaliação será feita com base nos seguintes elementos:

• exercícios a serem resolvidos em casa semanalmente (e entregues via Backboard) para cada uma das duas partes do curso. Esta componente de avaliação dará origem a uma nota final de, no máximo, 16 valores.
• um trabalho final opcional, envolvendo uma ou mais ferramentas estudadas no curso, para estudantes que desejam ter uma nota final superior a 16.

Docentes e Horário

Docente	Foto	Horário	Sala
Maria João Frade		5a-feira, 13h-16h	CP1 1.21
Jorge Sousa Pinto		5a-feira, 13h-16h	CP1 1.21

Alunos

#	Nome	Curso
a83916	Ana João Dias de Almeida	MiEI
a85516	António Manuel Carvalho Gonçalves	MiEI
a82529	Carlos Manuel Marques Afonso	MiEI
a34900	Cecília da Conceição de Oliveira Soares	MiEI
a67683	César Eduardo da Silva Magalhães	MiEI
pg41842	César Hugo Moreira da Silva	MEI
a80970	Davide da Silva Matos	MiEI
a76089	Etienne da Silva Filipe Amado da Costa	MiEI
a85731	Gonçalo José Azevedo Esteves	MiEI
a86617	Gonçalo Pinto Nogueira	MiEI
a81283	Hugo Filipe Oliveira de Sousa Faria	MiEI
a85573	Jorge Gabriel Alves Cerqueira	MiEI
a84776	José Emanuel Silva Rodrigues	MiEI
pg42839	José Gonçalo Macedo Costa	MEI
a84577	José Pedro Oliveira Silva	MiEI
a85954	Luís Mário Macedo Ribeiro	MiEI
a78566	Marcos Daniel Teixeira da Silva	MiEI
a71407	Maurício Zulueta Lima Salgado	MiEI
a85700	Pedro Miguel Araújo Costa	MiEI
a84783	Pedro Miguel Borges Rodrigues	MiEI
a86266	Rafael Inácio Lourenço	MiEI
a75411	Ricardo Guerra Leal	MiEI
a81716	Rodolfo António Vieira da Silva	MiEI
a80789	Rui Filipe Brito Azevedo	MiEI
pg36086	Vítor Hugo Gonçalves Silva	MMC