Aula 1 11/02
Objectivos da disciplina e tópicos do programa: verificação dedutiva de programas e verificação de sistemas reactivos pot model checking. Métodos de avaliação. Bibliografia recomendada.
Breve introdução aos métodos formais para o desenvolvimento de sistemas informáticos.
Breve introdução aos métodos formais para o desenvolvimento de sistemas informáticos.
Verificação de programas baseado em sistemas dedutivos. Lógicas de Floyd-Hoare baseadas em pré e pós condições. Correcção parcial e correcção total. Uma linguagem imperativa simples. Asserções e linguagem das condições. Sistema dedutivo para a correcção parcial. Exemplos.
Aula 3 21/02
Pre-condições fracas para o cálculo de correcção parcial. Tableaux para o sistema dedutivo para a correcção parcial. Invariantes de ciclo.Sistema dedutivo para a correcção parcial (cont.)
Aula 4 28/02
Cálculo de correção total. Variantes estritamente decrescentes. Regra para o comando while.
Uma arquitectura de um sistema de verificação de programas: mecanização do processo de dedução na lógica de Hoare. Lógica de Hoare orientada a objectivos. Pré-condições mais fracas. Algoritmo de geração de condições de verificação (VCGens) para a linguagem While com inteiros.
Uma arquitectura de um sistema de verificação de programas: mecanização do processo de dedução na lógica de Hoare. Lógica de Hoare orientada a objectivos. Pré-condições mais fracas. Algoritmo de geração de condições de verificação (VCGens) para a linguagem While com inteiros.
Complementar: Uma semântica operacional para a linguagem While. Integridade do sistema de correcção parcial.
Bibliografia:LICS Cap 4.1-4.3.2 , RSD cap 5.1-5.4,5.6, 6
Regras da Lógica de Hoare
Leituras complementares:
Fifty years of Hoare Logic
Early Search for Tractable Ways of Reasoning about Programs
Regras da Lógica de Hoare
Leituras complementares:
Fifty years of Hoare Logic
Early Search for Tractable Ways of Reasoning about Programs
Aula 5 3/03
Propriedades de Segurança. Lógica de Hoare com condições de segurança. Algoritmo de geração de condições de segurança. .Regras da lógica de Hoare para arrays. Exemplos. Algoritmo de geração de condições de verificação (VCGens) para a linguagem While com inteiros. Noções da extensão da Lógica de Hoare a procedimentos. Ferramentas de verificação de programas.
Aula 6 6/03
Introdução ao Dafny: paradigmas de programação e verificação estática de programas. Métodos. Funções e Predicados. Tipos de dados: básicos, arrays, coleções e classes. Tipos imutáveis e mutáveis (referências). Frames: acesso e modificação. Exemplos: recorrências de inteiros e pesquisa em arrays (linear e binária).
Bibliografia:
- Dafny online
- Github
- Install with VSCODE (or Emacs)
- Emacs- mode (boogie-friends)
- Extensão do VSCODE
- Dafny webpage
- Dafny Quick Reference
- Dafny Cheat Page
- Dafny Quick Reference (II)
- Dafny Manual Reference
- Tutorial para a escrita de programas em Dafny
- Dafny online
- Github
- Install with VSCODE (or Emacs)
- Emacs- mode (boogie-friends)
- Extensão do VSCODE
- Dafny webpage
- Dafny Quick Reference
- Dafny Cheat Page
- Dafny Quick Reference (II)
- Dafny Manual Reference
- Tutorial para a escrita de programas em Dafny
Aula 7 11/03
Introdução ao Dafny: continuação da aula anterior. Uso de lemas. Correção de algoritmos de ordenação. Coleções: conjuntos, sequências, multiconjuntos e mapas. Operações
Aula 8 17/03 (Video-conferência)
Introdução ao Dafny: Exemplo de correção duma implementação do Quicksort. Objectos em Dafny: Classes, construtores e métodos. DbC (design by contract) : contratos em Dafny: invariantes de classe, requisitos e garantias. O predicado Valid(). O atributo {:autocontracts}.
Apresentação de trabalhos práticos e resolução de programas em Dafny.
Design by Contract: exemplo de uma implementação dum DEQUE
Resolução de exercícios sobre verificação automática de programas em Dafny.
Aula 12 31/03 (Video-conferência)
Introdução ao Model checking. Sistemas de transição. Execuções. Modelação de circuitos sequências e programas.Paralelismo e Comunicação. Grafos de Programa. Exemplos
Bibliografia: Cap 1, 2.1 PMC
Paralelismo e Comunicação. Intercalagem de sistemas de de gratos de programa. Passagem de mensagens síncronas e assíncronas. Regras de construção de sistemas de transição. Produto síncrono.
Bibliografia: Cap 2.2.1-2.2.3-2.2.6 PMC
Tempo linear e ramificado. Lógica Temporal Linear. Semântica duma fórmula dado um sistema de transições. Satisfabilidade ao longo de um traço, dum caminho, num estado e num sistema. Equivalência de fórmulas. Especificação de propriedades usando fórmulas LTL.
Bibliografia: Cap 5.1- PMC, Cap. 3.2 LICS
Lógica Temporal Ramificada:CTL, lógica de árvores de computação. Semântica duma fórmula dado um sistema de transições. Satisfabilidade num estado e num sistema. Conjuntos de estados em que uma fórmula é satisfeita. Equivalência de fórmulas. Especificação de propriedades usando fórmulas CTL. Comparação entre LTL e CTL. CTL*: fórmulas de estado e de caminho; inclusão do LTL e do CTL.
Bibliografia: Cap 6.1—6.3, 6.8.1 PMC; Cap. 3.4,3.5 LICS
Exercícios Cap 6.1—6.3, 6.8.1 PMC
Apresentações do trabalho prático 1
Aula prática ; exercícios de LTL e CTL
Propriedades Temporais Lineares (LT). Deadlock. Caminhos e Traços. Invariantes e propriedades de segurança. Propriedades de vivacidade. Classificação de propriedades LT. Justeza.
Bibliografia: Cap 3.1-3.4 PMC
Continuação da aula anterior. Resolução de exercicios.
Bibliografia: Cap 3.1-3.4 PMC
Promela e o model checker SPIN. Processos, variáveis partilhadas, instruções guardadas: condicionais e ciclos. Verificação em SPIN: asserções, progresso, acessibilidade e justeza. Fórmulas LTL e "never claims". Exemplos de verificação de programas sequenciais e concorrentes. O interface ispin.
Entrega e Apresentação do trabalho prático 3
Comunicação por passagem de mensagens. Canais síncronos e asíncronos. Sistemas de transição de Sistemas de Canais. Canais em Promela. Exemplos: modelação Ciente-servidor; protocolos do bit alternado. Especificação de propriedades temporais lineares.
Algoritmos de Model Checking para o LTL usando Autómatos. Autómatos de Büchi. Propriedades das linguagens de palavras infinitas aceites por autómatos de Büchi. Sistemas de transições e autómatos de Büchi. Tradução de fórmulas LTL em Autómatos de Büchi. Never claims do SPIN e autómatos de Büchi.
Model checking simbólico. Definição de BDDs (binary decision diagrams). OBDDS: BDDs reduzidos e ordenados. Propriedades dos OBDDs. Algoritmos para a Construção de BDDS reduzidos. Expansão de Shannon para funções booleanas. Algoritmos apply, restrict e exists. Representação de conjuntos finitos com OBDDs. Representação de um modelo em OBDDs: conjunto de estados e relação de transição. Operações necessárias para o algoritmo de etiquetagem. Síntese de OBDDs.
Bibliografia: LICS Cap 6.1-6.3
