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

• Introduction
• Propositional Logic & SAT solvers
• First-Order Logic & Theories
• SMT solvers
• material pedagógico sobre Why3 e Frama-C disponível via Blackboard
• Deductive Reasoning & the Coq Proof Assistant (screencast videos disponíveis no Blackboard)
• Inductive Reasoning in Coq (screencast videos disponíveis no Blackboard)
• Programming and Proving in Coq ( screencast videos disponíveis no Blackboard)

Guiões

• SAT solving -- Ficheiros para a aula
• SMT solving -- Ficheiros para a aula
• Introdução à utilização do Z3 em Python: jupyter notebook, pdf, python
• Exemplo do Sudoku: jupyter notebook, pdf, python
• 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

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

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.