Aula 1/2 3/03
Objectivos da disciplina e tópicos do programa. Métodos de avaliação. Bibliografia recomendada.
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.
Brief introduction to formal methods.
Deductive program verification. Floyd-Hoare logic based on pre and post conditions. Assertions and logic of conditions. Parcial an d total correctness. A while imperative language. Deductive system of partial correctness.
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.
Brief introduction to formal methods.
Deductive program verification. Floyd-Hoare logic based on pre and post conditions. Assertions and logic of conditions. Parcial an d total correctness. A while imperative language. Deductive system of partial correctness.
Bibliografia: Cap. 1 e 2 RSD, Slides,
LICS Cap 4.1-4.3.2 , RSD cap 5.1-5.4
Regras da Lógica de Hoare/ Hoare logic rules
LICS Cap 4.1-4.3.2 , RSD cap 5.1-5.4
Regras da Lógica de Hoare/ Hoare logic rules
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. Uma semântica operacional para a linguagem While. Integridade do sistema de correcção parcial. Cálculo de correção total. Variantes estritamente decrescentes. Regra para o comando while.
Weakest preconditions (wp). Tableaux for the partial correctness calculus using wp. A natural semantics for the while language. Soundness of the partial correctness calculus. Total correctness calculus. Variants. Rule for the while statement.
Weakest preconditions (wp). Tableaux for the partial correctness calculus using wp. A natural semantics for the while language. Soundness of the partial correctness calculus. Total correctness calculus. Variants. Rule for the while statement.
O problema a adaptação de tripos de Hoare. Mecanização do calculo de correção parcial.
O cálculo sem regra da consequência (H_g) e o cálculo das pré-condições mais fracas. Equivalência do cálculo H e do cálculo H_g. Algoritmo de geração de condições de verificação (VCGen). Adequação do algoritmo VCGen ao cálculo H_g. Exemplos
The Adaptation problem for Hoare logic. Mechanisation of the partial correctness calculus. Calculus without cons: H_g. Equivalence of H and H_g. Weakest preconditions (wp). Verification condition generator: VCGen. Correctness of VCGem. Examples.
O cálculo sem regra da consequência (H_g) e o cálculo das pré-condições mais fracas. Equivalência do cálculo H e do cálculo H_g. Algoritmo de geração de condições de verificação (VCGen). Adequação do algoritmo VCGen ao cálculo H_g. Exemplos
The Adaptation problem for Hoare logic. Mechanisation of the partial correctness calculus. Calculus without cons: H_g. Equivalence of H and H_g. Weakest preconditions (wp). Verification condition generator: VCGen. Correctness of VCGem. Examples.
Propriedades de segurança. Semântica operacional com erro e programas seguros: Asserções safe(E). Arrays com indices limitados: programas seguros e geração de condições de verificação. Procedimentos sem parâmetros e recursão.
Safety properties: error semantics and safe programs. Bounded arrays : safe programs and verification condition generator. Procedures without parameter and recursion.
Safety properties: error semantics and safe programs. Bounded arrays : safe programs and verification condition generator. Procedures without parameter and recursion.
Exercícios:
Aula 9/10 31/03
Apresentação do primeiro trabalho prático.
Frameworks para a geração de condições de verificação.
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). Correção de algoritmos de ordenação. Coleções: conjuntos, sequências, multiconjuntos e mapas. Operações. Uso de lemas.
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). Correção de algoritmos de ordenação. Coleções: conjuntos, sequências, multiconjuntos e mapas. Operações. Uso de lemas.
Bibliografia:
Linguagem de anotações Dafny
- Dafny site
- 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
- Types in Dafny
- Tutorial para a escrita de programas em Dafny
Linguagem de anotações Dafny
- Dafny site
- 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
- Types in Dafny
- Tutorial para a escrita de programas em Dafny
Design by Contract.: Classes com pré e pós condições. Invariante de classe: predicado Valid(). Herança. Abstração e variáveis e funções ghost. Exemplos: stacks, conjuntos e dequeues.
Bibliografia:
Linguagem de anotações Dafny
The Dafny Integrated Development Environment
Developing Verifies Programs with Danny
The Dafny Integrated Development Environment
Accessible Software Verification with Dafny
Linguagem de anotações Dafny
The Dafny Integrated Development Environment
Developing Verifies Programs with Danny
The Dafny Integrated Development Environment
Accessible Software Verification with Dafny
Aula 15/16 - 28/04
Continuação da aula anterior. Resolução de exercícios
Bibliografia:
Linguagem de anotações Dafny
The Dafny Integrated Development Environment
Developing Verifies Programs with Danny
The Dafny Integrated Development Environment
Accessible Software Verification with Dafny
Linguagem de anotações Dafny
The Dafny Integrated Development Environment
Developing Verifies Programs with Danny
The Dafny Integrated Development Environment
Accessible Software Verification with Dafny
Ferramentas de prova. Demonstradores automáticos de teorias decidíveis.
Resolutores SMT baseados em resolutores SAT. Algoritmo de David-Putman para a satisfazibilidade de fórmulas proposicionais. Resolutores DPLL baseados em CDCL (conflict driven clause learning). Grafo das implicações e análise de conflitos.
Teorias da lógica de primeira ordem. Teorias decidíveis. Integração com resolutores SAT. Introdução ao Z3 usando Z3py.
Resolutores SMT baseados em resolutores SAT. Algoritmo de David-Putman para a satisfazibilidade de fórmulas proposicionais. Resolutores DPLL baseados em CDCL (conflict driven clause learning). Grafo das implicações e análise de conflitos.
Teorias da lógica de primeira ordem. Teorias decidíveis. Integração com resolutores SAT. Introdução ao Z3 usando Z3py.
Bibliografia:
Decision Procedures (DP) (2nd Ed): Cap.1. 2.1, 2,2.1-2.2.4
The Calculus of Computation
SATLIVE
SAT association
SMT-LIB
Z3 : code
Exemplos
Z3py: pip install z3-solver
Decision Procedures (DP) (2nd Ed): Cap.1. 2.1, 2,2.1-2.2.4
The Calculus of Computation
SATLIVE
SAT association
SMT-LIB
Z3 : code
Exemplos
Z3py: pip install z3-solver
Exercícios:
Resolutores SMT usando SAT: DPLL(T) lazy usando algoritmos decidiveis para conjunção de fórmulas atómicas de de teorias T.
Lógica equacional e teoria das funções não interpretadas(EUF). Redução de fórmulas EUF à lógica equacional: método de Ackerman. Algoritmo para a decisão duma conjunção de igualdades e funções não interpretadas.
Teoria dos arrays. Redução à teoria das funções não interpretadas.
Lógica equacional e teoria das funções não interpretadas(EUF). Redução de fórmulas EUF à lógica equacional: método de Ackerman. Algoritmo para a decisão duma conjunção de igualdades e funções não interpretadas.
Teoria dos arrays. Redução à teoria das funções não interpretadas.
Bibliografia:
Decision Procedures (DP) (2nd Ed): Cap.3.1-3.3, 4.1-4.4, 7.1-7.3
The Calculus of Computation (axiomatizações de teorias e resolutores)
SATLIVE
SAT association
SMT-LIB
Z3 : code
Exemplos
Z3py: pip install z3-solver
notebooks
Decision Procedures (DP) (2nd Ed): Cap.3.1-3.3, 4.1-4.4, 7.1-7.3
The Calculus of Computation (axiomatizações de teorias e resolutores)
SATLIVE
SAT association
SMT-LIB
Z3 : code
Exemplos
Z3py: pip install z3-solver
notebooks
Exercícios:
Aula 20 - 19/05
Apresentação do segundo trabalho prático.
Dedução natural para a lógica proposicional usando sequentes. Noção de lógica intuicionistica. Fragmento implicacional da lógica proosicional intuicionista (IPC(->)). Revisão do lambda-calculus puro e sistema de tipos simples. Isomorfismo de Curry-Howard.
Introdução ao demonstrador interactivo Coq usando tipos simples IPC(->). Tipos: Prop e Set. Táticas: intro, apply e assumption.
O interface coqide.
Introdução ao demonstrador interactivo Coq usando tipos simples IPC(->). Tipos: Prop e Set. Táticas: intro, apply e assumption.
O interface coqide.
Bibliografia:
Curry-Howard Isomorphism
Lectures on the Curry-Howard Isomorphism (M. Sorensen & P. Urzyczyn) )Cap 2-4
Interactive Theorem Proving: Cap 1-3.
Coq prover
Manual
Online
Curry-Howard Isomorphism
Lectures on the Curry-Howard Isomorphism (M. Sorensen & P. Urzyczyn) )Cap 2-4
Interactive Theorem Proving: Cap 1-3.
Coq prover
Manual
Online
Dedução natural para a lógica primeira ordem (intuicionista) usando sequentes. Noção de tipos dependentes e Regra do produto. Isomorfismo de Curry-Howard para tipos dependentes e lógica de primeira ordem intuicionistica.
Tipos dependentes em Coq. Dedução natural de fórmulas de lógica de primeira ordem em Coq. Tácticas de introdução e eliminação de conectivas/quantificadores/=: intro, apply, split, right, left, exists, reflexivity e rewrite. Tipos indutivos: simples e recursivos. Princípios de indução. Conectivas lógicas como tipos indutivos. Naturais de Peano como tipos indutivos.
Tipos dependentes em Coq. Dedução natural de fórmulas de lógica de primeira ordem em Coq. Tácticas de introdução e eliminação de conectivas/quantificadores/=: intro, apply, split, right, left, exists, reflexivity e rewrite. Tipos indutivos: simples e recursivos. Princípios de indução. Conectivas lógicas como tipos indutivos. Naturais de Peano como tipos indutivos.
Bibliografia:
Lectures on the Curry-Howard Isomorphism (M. Sorensen & P. Urzyczyn) )Cap 9-10
Interactive Theorem Proving: Cap 4-6.
Coq prover
Manual
Online
Exemplos
Resumo de tácticas
Lectures on the Curry-Howard Isomorphism (M. Sorensen & P. Urzyczyn) )Cap 9-10
Interactive Theorem Proving: Cap 4-6.
Coq prover
Manual
Online
Exemplos
Resumo de tácticas
Aula 25-26 - 09/06/2022
Tipos indutivos em Coq (cont). Tácticas: induction, pattern, elim, case e constructor. Pattern matching para definir funções por casos. Funções sobre tipos indutivos recursivos: Fixpoint. Tácticas discriminate, injection e inversion. Tipos indutivos polimórficos e dependentes: listas e árvores. Predicados indutivos. Exemplo da formalização e correção da ordenação por inserção numa lista. Extração de programas correctos para Haskell.