Verificação Formal

2021/22

(Em actualização)

Nesta UC são abordadas técnicas clássicas de verificação de software, quer automáticas quer interactivas, apoiadas na utilização de três das ferramentas mais utilizadas para este fim. As técnicas são estudadas de forma complementar e ilustradas por um conjunto de casos de estudo que incluem programas/algoritmos funcionais, imperativos, e distribuídos.

O programa começa por uma introdução ao assistente de prova Coq e ao sistema de tipos que lhe é subjacente. Trata-se de uma ferramenta muito madura e que tem tido inúmeras aplicações em diversos domínios, nomeadamente na verificação “hard” de software — casos de sucesso de grande repercussão incluem a prova mecanizada do teorema das 4 cores ou a certificação integral de um compilador para a linguagem de programação C.

Segue-se o estudo do verificador Why3, uma ferramenta polivalente que oferece uma linguagem de programação ML e uma lógica de primeira ordem, com tipos indutivos e polimorfismo. As linguagens são integradas de uma forma que suporta a verificação de algoritmos com base em lógica de Hoare, e também a utilização de programas no desenvolvimento de provas ao nível lógico. O Why3 funciona simultaneamente como front-end para as mais variadas ferramentas de prova (incluindo SMT solvers) constituindo desta forma uma plataforma única para a verificação de software baseada, sempre que possível, em prova automática.

Finalmente, a suite TLA+ é também uma ferramenta clássica e de grande repercussão, adoptada em anos recentes na verificação de software altamente complexo por parte de empresas como a Amazon. Apesar de incluir também um núcleo de lógica de primeira ordem e suporte para prova automática, o que distingue esta ferramenta das anteriores é por um lado a utilização de lógica temporal e da noção de “refinamento”, utilizado por exemplo no estabelecimento da relação entre especificações e implementações, e por outro a existência de um “model checker” para a exploração algorítmica (automática) dos estados de um sistema.

Programa

• Verificação Dedutiva e Prova Assistida
  • Dedução natural. Proposições como tipos.
  • O sistema de prova Coq.
  • Correção de programas funcionais.
  • Extração de programas.
• Verificação de Software com Why3
  • Linguagem lógica, polimorfismo e tipos indutivos
  • Prova ao nível lógico: abordagem “multi-prover”; utilização do IDE e de transformações de prova; provas indutivas; reprodução de provas.
  • Linguagem de programas WhyML. Mutabilidade; modularidade: clonagem de módulos
  • Prova ao nível dos programas: contratos e anotações; condições de verificação; extracção de programas
  • Casos de estudo: provas sobre programas funcionais, programas imperativos, e programas distribuídos
• Model Checking
  • Lógica temporal linear (LTL) e de tempo ramificado (CTL)
  • Model checking explícito e simbólico
  • Bounded model checking simbólico
  • Linguagens de modelação e especificação: SMV, TLA, Alloy
  • Ferramentas de verificação: NuSMV, nuXmv, TLC, Alloy Analyzer

Docentes

• Jorge Sousa Pinto (JSP)
• Maria João Frade (MJF)
• Alcino Cunha (MAC)

Avaliação

• Três provas de avaliação (testes) + exame de recurso.
• As notas acima de 17 valores (quer na avaliação contínua, quer no exame) terão que ser defendidas através da realização de um pequeno projecto.

Horário

Tipo	Horário	Sala
Teórica	6ªf. 9h-11h	Ed.1 1.19
Teórico-prática	6ªf. 11h-12h	Ed.1 1.19

Planificação

#	Data	Docentes	Sumário
1		MJF	Dedução Natural. Proposições como tipos. Introdução ao sistema de prova assistida Coq.
2		MJF	Tipos indutivos e seus eliminadores. Provas por indução em Coq.
3		MJF	Correção de programas funcionais. Extração de programas.
4		MJF	Teste laboratorial de Coq.
5		JSP	Why3: Lógica e verificação de programas imperativos
6		JSP	Why3: Verificação de programas funcionais
7		JSP	Why3: Verificação de sistemas distribuídos
8		JSP	Why3: Teste
9		MAC	Model Checking: estruturas de Kripke, logica temporal linear (LTL), introdução ao nuXmv e TLA+.
10		MAC	Model Checking: lógica temporal de tempo ramificado (CTL), LTL vs CTL, safety vs liveness, condições de justiça.
11		MAC	Model Checking: verificação explícita de CTL, verificação simbólica de CTL, verificação explícita de LTL.
12		MAC	Model Checking: esclarecimento de dúvidas.
13		MAC	Model Checking: teste.
		MAC, MJF, JSP	Exame.
		MAC, MJF, JSP	Projecto.

Material

Slides

• Deductive Verification and the Coq Proof Assistant
• Inductive Reasoning in Coq
• Programming and Proving in Coq
• Why3 Slides
• Model Checking

Exercícios

• lesson1.v
• Ficha Coq(1)
• lesson2a.v
• lesson2b.v
• Ficha Coq(2)
• lesson3.v
• Ficha Coq(3)
• Model Checking

Testes

• Model Checking

Exemplos

• Why3 examples
• TLA+ examples
  • Peterson Mutual Exclusion for N processes

Bibliografia

• Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Yves Bertot & Pierre Casteran. Springer, 2004.
• Software Foundations. Benjamin Pierce et al., 2007, with regular updates.
• The Why3 Platform François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. Version 1.4, March 2021
• Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Leslie Lamport. Addison-Wesley, 2002.
• Principles of Model Checking. Christel Baier and Joost-Pieter Katoen. The MIT Press, 2008.

Outras leituras recomendadas

• Yves Bertot. Coq in a Hurry. INRIA, 2015.
• …

Ferramentas

• The Coq Proof Assistant (disponível no Opam)
  • Recomendado instalar: CoqIde (disponível no Opam)
  • The jsCoq Interactive Online System!
• Why3 (disponível no Opam)
  • Recomendado instalar alguns solvers, em particular Alt-ergo (disponível no Opam) e CVC4
• TLA+ Toolbox
• nuXmv