| Aula | Data | Sumário | Bib |
|---|---|---|---|
| 1 | 18/2 | Objectivos da disciplina e tópicos do programa. Métodos de avaliação. Bibliografia recomendada. Motivação para os métodos formais e diversas abordagens da verificação formal. | LICS Cap 3.1, PMC Cap. 1, RSD Cap 1-2 |
| 2 | 21/2 | Verificação por modelos (model checking). Lógica temporal linear (LTL). Sistemas de transições e modelos de Kripke. Semântica da LTL. Exemplos | LICS Cap 3.2.1, 3.2.2
Complementar PMC Cap. 2.1, 2,2, 3, 5.1.1 51.2 |
| 3 | 25/2 | Especificação de propriedades em LTL. Equivalência semântica de fórmulas LTL. Conjunto completos de conectivas. | LICS Cap 3.2.3-5 PMC Cap 5. pp 229-257 |
| 4 | 28/2 | Exemplo de Model checking: exclusão mútua. Especificação de propriedades e modelação. Utilização da aplicação NuSMV para model checking. Linguagem de especificação de modelos: variáveis e módulos. Estados. Especificação de propriedades. Computação síncrona e assíncrona. Exemplos. | LICS Cap 3.3.1, 3.3.3 NuSMV |
| 5 | 5/3 | Uso interactivo do NuSMV. Fairness. Traços. | NuSMV |
| 6 | 7/3 | Lógica de tempo ramificado (CTL). Semântica do CTL. Especificação de propriedades em CTL e em LTL (exemplos). Equivalência semântica de fórmulas de CTL. | LICS Cap 3.4.1-4 PMC Cap 6. pp 313-334 |
| 7 | 12/3 | Especificação de modelos e de propriedades em CTL e em LTL (exemplos). Expressividade do CTL vs. LTL. CTL* | LICS Cap 3.4.5, 3.5 PMC Cap 6.3 |
| 8 | 14/3 | Algoritmo de model checking para CTL por etiquetagem de estados. Exemplo. Optimização usando a conectiva EG | LICS Cap pp 221-225 PMC Cap 6.4.1 |
| 9 | 19/3 | Algoritmo de model checking para o CTL por etiquetagem de estados (cont.). Model cheking com fairness. Correção e Terminação. | LICS Cap pp 225-232, 238-245 PMC Cap 6.4 |
| 10 | 21/3 | 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. | LICS Cap 6 pp 358-373 PMC Cap. 6.7.1, 6.7.3 |
| 11 | 02/04 | 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 necesárias para o algoritmo de etiquetagem. Síntese de OBDDs. | LICS Cap 6 pp 374-388, Intro. BDDs |
| 11a | 05/04 | Continuação da aulas anterior. Resolução de exercícios. | LICS Cap 6 pp 374-388, Intro. BDDs |
| 12 | 09/04 | Autómatos finitos não determinísticos e autómatos finitos de Büchi. Autómatos Finitos Alternados. | Automata-Theoretic Approach to LTL, M. Vardi |
| 13 | 11/4 | Autómatos de Büchi alternados. Autómato de Büchi e Autómato de Büchi alternado associados a uma fórmula do LTL, AF. Autómato de Büchi associado a um modelo. Algoritmo de model checking para o LTL. | Automata-Theoretic Approach to LTL, M. Vardi |
| 14 | 16/4 | 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. 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. Exemplos. | LICS Cap 4.1-4.3.2 , RSD cap 5.1-5.4 |
| 15 | 23/4 | Uma semântica operacional para a linguagem While. Integridade do sistema de correcção parcial. Incompletude do sistema de correcção parcial. | W93 Cap. 6 e 7 |
| 16 | 30/4 | Regras de Lógica de Hoare para ciclos for e arrays. Exemplos. Cálculo de correção total. Variantes estritamente decrescentes. Regra para o comando while. | LICS ; RSD 5.5 e 5.6 | 17 | 02/5 | 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. | RSD Cap. 6 |
| 18 | 14/5 | Propriedades de segurança. Uma semântica operacional para a linguagem While com inteiros e arrays de tamanho limitado, considerando a noção de erro. Lógica de Hoare com condições de segurança. Algoritmo de geração de condições de segurança. Noções da extensão da Lógica de Hoare a procedimentos. | RSD Cap. 7, Cap.8 |
| 19 | 16/5 | Linguagem de especificação ACSL: comportamentos, contratos funcionais axiomatizações. Exemplos. Plataforma frama-C e plugin jessie. Verificação de segurança e funcional. Exemplos. | Frama-c,
Jessie, ACSL, Why3 RSD Cap. 9 |
| 20 | 21/5 | Plataforma frama-C e plugin jessie. Verificação de segurança e funcional. Exemplos. |
Examples RSD CAP 9 |
| 21 | 23/5 | Plataforma frama-C e plugin jessie (cont). Verificação de segurança e funcional. Exemplos. |
Partition RSD CAP 10 |
| 22 | 28/5 | Demonstradores automáticos de teoremas baseados em SAT-DPLL e teorias decidíveis: inteiros, reais, ``arrays'', etc. SMTs e algoritmos decisão. |
SMT-LIB Decision Procedures Cap 1,2 ,11 |