Verificação Formal

2024/25

Em UCs passadas, nomeadamente em MFES, já foi abordada a verificação dedutiva de algoritmos imperativos sequenciais e de algoritmos funcionais. Nesta UC serão abordadas técnicas para especificação e verificação de algoritmos não sequenciais, nomeadamente algoritmos concorrentes, self-stabilizing e distribuídos.

Na primeira parte será abordada a especificação de algoritmos usando TLA+, uma linguagem introduzida por Leslie Lamport precisamente com o objectivo de simplificar a especificação de algoritmos não sequenciais. As especificações em TLA+ podem ser verificadas automaticamente com o model-checker TLC, e esta abordagem lightweight fez com que o TLA+/TLC tenha sido frequentement adoptado pela indústria (e.g. Amazon) para verificar algoritmos complexos.

Na segunda parte será abordada a verificação dedutiva destes mesmos algoritmos, técnica que permitirá verificar a sua correção para qualquer configuração possível, o que não é possível com o model-checking que apenas pode ser usado para verificar um conjunto de configurações limitado. Para tal será usado o Why3, já previamente introduzido em MFES, uma ferramenta que usa SMT solvers para efectuar a prova automática das condições de verificação inerentes à verificação dedutiva.

Programa

• Especificação e verificação de algoritmos não sequenciais (concorrentes, self-stablizing e distribuídos)
• Model-checking com TLA+/TLC
• Verificação dedutiva com Why3

Docentes

• Alcino Cunha (MAC)
• Jorge Sousa Pinto (JSP)

Avaliação

• Avaliação contínua com duas provas de avaliação:
  • Teste individual escrito sobre model-checking (50%)
  • Teste individual escrito sobre verificação dedutiva (50%)
• O exame de recurso terá duas partes com as mesmas cotações
• As notas iguais ou superiores a 19 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	4ªf. 9h-11h	CP2 2.11
Teórico-prática	4ªf. 11h-12h	CP2 2.11

Planificação

#	Data	Docentes	Sumário
1	5 Fev	MAC	Introdução ao TLA+.
2	12 Fev	MAC
3	19 Fev	MAC
4	26 Fev	MAC
5	5 Mar	MAC
6	12 Mar	MAC
7	19 Mar	MAC	1º Teste
8	26 Mar	JSP
9	2 Abr	JSP
10	9 Abr	JSP
11	23 Abr	JSP
12	30 Abr	JSP
13	7 Mai	JSP
14	28 Mai	JSP	2º Teste
	16 Jun	MAC+JSP	Exame

Material

Bibliografia

• Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Leslie Lamport. Addison-Wesley, 2002.
• The TLA+ Video Course. Leslie Lamport. 2021.
• The Why3 Platform François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. Version 1.4, March 2021

Outras leituras recomendadas

• Shankar, A. U.: An introduction to assertional reasoning for concurrent systems. ACM Computing Surveys (CSUR), 25(3), 225-262, 1993.
• Leslie Lamport. If You’re Not Writing a Program, Don’t Use a Programming Language. Bulletin of EATCS, 125, June 2018.

Ferramentas

• TLA+ Toolbox
• Why3