1 Informações importantes

• Data de apresentação: 05 e 07 de maio
• Trabalho individual ou em dupla
• Enviar slides no moodle (em PDF)
• Tempo de apresentação: 15 minutos (dupla) ou 10 minutos (individual)

2 Introdução

Existe uma variedade de técnicas e ferramentas de métodos formais, e seria inviável aprender várias delas nesta disciplina. O objetivo deste seminário é explorar superficialmente outras técinas/ferramentas para a compreensão dessa variedade e das possíveis alternativas.

3 Sugestões de Tópicos

Dentro da técnica de model checking que temos estudado, existem várias outras ferramentas (além de TLA+ e Quint):

• PlusCal (versão "imperativa" de TLA+)
• Alloy
• NuSMV
• Spin
• Redes de Petri
• PRISM
• P
• Mais na lista do Wikipedia

Uma técnica que já mencionamos na disciplina algumas vezes é a de assistentes de provas. Seguem algumas ferramentas:

• Coq
• Isabelle
• Agda
• Lean (brasileiro!)
• Idris
• Dafny
• F*
• Mais na lista do Wikipedia

Ferramentas para verificação de programas escritos em linguagens de programação:

• Dafny
• Viper
• Prusti (para Rust)
• Gobra (para Go)
• Nagini (para Python)

Outras técnicas (além de model checking e assistentes de provas):

• Máquina de estado abstrata (Abstract State Machine - ASM)
• Calculo \(\pi\) (π-calculus)
• Continuation Passing Style (CSP)
• Lógica de Hoare
• Método de desenvolvimento Viena (Vienna Development Method - VDM)

4 Estrutura

O enfoque da apresentação deve ser a técnica/ferramenta em si: como usá-la, para que é boa, para que é ruim, em que(ais) área(s) é mais aplicada. Desejável: casos de uso (i.e. empresa X usou pra verificar Y). Indesejável: Detalhes históricos.

• Mostre ao menos um exemplo (código/fórmula)