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. Partial and 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. Partial and total correctness. A while imperative language. Deductive system of partial correctness.
Bibliografia/Bibliography
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
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
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.
Bibliografia/Bibliography:
LICS Cap 4.1-4.3.2 , RSD cap 5.1-5.6, SWA 2.1. , 9.2, 9.3 10.1
Regras da Lógica de Hoare
LICS Cap 4.1-4.3.2 , RSD cap 5.1-5.6, SWA 2.1. , 9.2, 9.3 10.1
Regras da Lógica de Hoare
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 VCG 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: VCG. Correctness of VCG with respect to H_g. 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 VCG 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: VCG. Correctness of VCG with respect to H_g. 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:
Contratos e recursão mútua. Sistema dedutivo axiomático para procedimentos sem parâmetros. Geração de condições de verificação. Frame conditions. Procedimentos com parâmetros. Sistema dedutivo axiomático para procedimentos com parâmetros passados por valor.
Exemplos
Apresentação do primeiro trabalho prático.
Contracts and mutual recursion. Programming with contracts. Inference System for Paremeterless Procedures . Verification Conditions for Paremeterless Procedures . Frame conditions. Procedures with Parameters. Inference System for Procedures with Parameters passed by Value. Examples
Presentation of the written assignment.
Exemplos
Apresentação do primeiro trabalho prático.
Contracts and mutual recursion. Programming with contracts. Inference System for Paremeterless Procedures . Verification Conditions for Paremeterless Procedures . Frame conditions. Procedures with Parameters. Inference System for Procedures with Parameters passed by Value. Examples
Presentation of the written assignment.
Bibliografia/Bibliography: RSD cap 8.2-8.4
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.
Frameworks for the generation of verification conditions (VCG).Dafny: programming languages with static verification of programs. Methods. Functions and Predicates. Types: basic, arrays, collections and classes. Immutable and mutable (references) types. Frames: reads and modifies. Exemples with integers and arrays. Verification of Sorting algorithms. Collections: sets, multistep, sequences, maps. Operatiosn. Use of lemmas to proof theorems with Dafny.
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.
Frameworks for the generation of verification conditions (VCG).Dafny: programming languages with static verification of programs. Methods. Functions and Predicates. Types: basic, arrays, collections and classes. Immutable and mutable (references) types. Frames: reads and modifies. Exemples with integers and arrays. Verification of Sorting algorithms. Collections: sets, multistep, sequences, maps. Operatiosn. Use of lemmas to proof theorems with Dafny.
Bibliografia/Bibliography:
Linguagem de anotações Dafny
Program Proofs, K. Leino Cap/Chap. 1,11-15
- Dafny site
- Github
- Install with VSCODE (or Emacs)
- Emacs- mode (boogie-friends)
- Extensão do VSCODE
- Dafny Tutorial online
- Dafny Quick Reference
- Dafny Cheat Page
- Dafny Quick Reference (II)
- Dafny Manual Reference
- Types in Dafny
- Tutorial Dafny
Linguagem de anotações Dafny
Program Proofs, K. Leino Cap/Chap. 1,11-15
- Dafny site
- Github
- Install with VSCODE (or Emacs)
- Emacs- mode (boogie-friends)
- Extensão do VSCODE
- Dafny Tutorial online
- Dafny Quick Reference
- Dafny Cheat Page
- Dafny Quick Reference (II)
- Dafny Manual Reference
- Types in Dafny
- Tutorial Dafny
Exercícios/Exercices:
Verificação de programas imperativos com Dafny
Exemplos/Examples
From Program Proofs
Verificação de programas imperativos com Dafny
Exemplos/Examples
From Program Proofs
Datatypes em Dafny: construtores, destrutores e encaixe de padrões. Programação funcional: Listas e outros tipos indutivos. Provas por indução na estrutura do tipo indutivo. Lemas e calc.
Design by Contract.: Classes com pré e pós condições. Invariante de classe: predicado Valid(). Directivas: reads, modifies; old() e fresh(). Herança.
Datatypes in Dafny: constructors, destructors and pattern matching. Functional programming on Dafny. Lists and other inductive types. Proofs by induction. Lemmas and calc.
Design by Contract. Classes with contracts: pre and post conditions. Class invariants: predicate Valid(). Directives:reads and modifies; old() and fresh(). Inheritance.
Design by Contract.: Classes com pré e pós condições. Invariante de classe: predicado Valid(). Directivas: reads, modifies; old() e fresh(). Herança.
Datatypes in Dafny: constructors, destructors and pattern matching. Functional programming on Dafny. Lists and other inductive types. Proofs by induction. Lemmas and calc.
Design by Contract. Classes with contracts: pre and post conditions. Class invariants: predicate Valid(). Directives:reads and modifies; old() and fresh(). Inheritance.
Bibliografia/Bibliograpy:
Linguagem de anotações Dafny
Program Proofs, K. Leino Cap/Chap. 4-8, 16
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
Program Proofs, K. Leino Cap/Chap. 4-8, 16
The Dafny Integrated Development Environment
Developing Verifies Programs with Danny
The Dafny Integrated Development Environment
Accessible Software Verification with Dafny
Invariantes de estruturas de dados: funcionais e de estado. Abstração, variáveis e funções ghosts. Tipos de dados abstratos: representação, modelo e invariantes. Exemplos: vários tipos de filas e conjuntos.
Datatype invariants: functional and stateful. Abstractions, ghost variables and ghost functions. Abstract data types (ADT): representation (dynamic frames), model and invariants. Examples: Queues and sets.
Datatype invariants: functional and stateful. Abstractions, ghost variables and ghost functions. Abstract data types (ADT): representation (dynamic frames), model and invariants. Examples: Queues and sets.
Ferramentas de prova.
Resolutores SAT. Transformação de Tseitin. Algoritmo de David-Putman para a satisfazibilidade de fórmulas proposicionais em CNF. Resolutores DPLL baseados em CDCL (conflict driven clause learning). Grafo das implicações (BCP) e análise de conflitos: aprendizagem de cláusulas. Resolutores SAT modernos. PySAT. Modelação de problemas em SAT.
Proof frameworks. SAT solvers. Tseitin's Transformation for CNF encodings. David-Putman algorithm for CNF. DPLL-CDCL Solvers (Conflict driven clause learning). Implication Graph and Bounded constraint propagation. Conflict analyses: learned clause and backtrack level. Modern SAT solvers. PySAT. Modeling problems in SAT.
Resolutores SAT. Transformação de Tseitin. Algoritmo de David-Putman para a satisfazibilidade de fórmulas proposicionais em CNF. Resolutores DPLL baseados em CDCL (conflict driven clause learning). Grafo das implicações (BCP) e análise de conflitos: aprendizagem de cláusulas. Resolutores SAT modernos. PySAT. Modelação de problemas em SAT.
Proof frameworks. SAT solvers. Tseitin's Transformation for CNF encodings. David-Putman algorithm for CNF. DPLL-CDCL Solvers (Conflict driven clause learning). Implication Graph and Bounded constraint propagation. Conflict analyses: learned clause and backtrack level. Modern SAT solvers. PySAT. Modeling problems in SAT.
Bibliografia:
Decision Procedures (DP) (2nd Ed): Cap.1, 2.1-2.2
Handbook of Satisfiability (Cap 1-4) (Complementary)
SATLIVE
SAT association
SMT-LIB
PySAT: pip install python-sat (and pip install py-aiger-cnf)
notebooks
Decision Procedures (DP) (2nd Ed): Cap.1, 2.1-2.2
Handbook of Satisfiability (Cap 1-4) (Complementary)
SATLIVE
SAT association
SMT-LIB
PySAT: pip install python-sat (and pip install py-aiger-cnf)
notebooks
Aula 19/20 - 19/05
Demonstradores automáticos de teorias decidíveis. Teorias da lógica de primeira ordem. Noção de teoria e aciomatixação. Algumas teorias:igualdade r funções não interpretadas; aritmética; inteiros; reais e racionais; listas;arrays; etc . Teorias decidíveis e fragmentos de teorias . Composição de teorias. Integração com resolutores SAT. Resolutores SMT usando SAT: DPLL(T) lazy usando algoritmos decidiveis para conjunção de fórmulas atómicas de de teorias T. Introdução ao Z3 usando Z3py
Automatic solvers for decidable theories. First-order logic theories. Notion of theory and axiomatisation. Some examples of theories: equational, uninterpreted functions; arithmetic (naturals); integers; reals; lists; arrays bit-vectores. Decidable theories and fragments of theories. Composition of theories.SAT based SMT solvers: lazy and eager. Introduction to Z3 and Z3py.
Automatic solvers for decidable theories. First-order logic theories. Notion of theory and axiomatisation. Some examples of theories: equational, uninterpreted functions; arithmetic (naturals); integers; reals; lists; arrays bit-vectores. Decidable theories and fragments of theories. Composition of theories.SAT based SMT solvers: lazy and eager. Introduction to Z3 and Z3py.
Bibliografia:
Decision Procedures (DP) (2nd Ed): Cap. 3.1-3.4
The Calculus of Computation (axiomatizações de teorias e resolutores): Cap. 3
SMT-LIB
SMT-COMP
Z3 : guide
Z3 internals
Z3 tutorial
Exemplos
Z3py: pip install z3-solver
notebooks
Decision Procedures (DP) (2nd Ed): Cap. 3.1-3.4
The Calculus of Computation (axiomatizações de teorias e resolutores): Cap. 3
SMT-LIB
SMT-COMP
Z3 : guide
Z3 internals
Z3 tutorial
Exemplos
Z3py: pip install z3-solver
notebooks
Exercícios:
- Ver os exemplos no notebook Z3Python
- Seguir os tutoriais em:
https://ericpony.github.io/z3py-tutorial/guide-examples.htm
- formaliza e testa uma especificação para resolver puzzles Sudoku
- Ver os exemplos no notebook Z3Python
- Seguir os tutoriais em:
https://ericpony.github.io/z3py-tutorial/guide-examples.htm
- formaliza e testa uma especificação para resolver puzzles Sudoku
Lógica equacional e teoria das funções não interpretadas(EUF). Algoritmo para a decisão duma conjunção de igualdades e funções não interpretadas. Redução de fórmulas EUF à lógica equacional: método de Ackerman. Algoritmo "eager" para a lógica equacional: grafos de igualdades e método esparso com grafo não polar.
Teoria dos arrays. Redução à teoria das funções não interpretadas. Propriedades de arrays.
Equality logic and uninterpreted functions (EUF).Decision algorithm for the conjunction
of equalities (and disequalities) and uninterptred functions with congruence closure. Reduction of EUF formulas to equality logic: Ackermann reduction. Eager algorithm for equational logic: equally graphs and sparse method with nonpolar graph. Theory of arrays (decidable fragment). Reduction to the theory of uninterpreted functions. Properties of arrays.
Teoria dos arrays. Redução à teoria das funções não interpretadas. Propriedades de arrays.
Equality logic and uninterpreted functions (EUF).Decision algorithm for the conjunction
of equalities (and disequalities) and uninterptred functions with congruence closure. Reduction of EUF formulas to equality logic: Ackermann reduction. Eager algorithm for equational logic: equally graphs and sparse method with nonpolar graph. Theory of arrays (decidable fragment). Reduction to the theory of uninterpreted functions. Properties of arrays.
Bibliografia:
Decision Procedures (DP) (2nd Ed): Cap. 11.1-11.5, 4.1-4.4, 7.1-7.3
The Calculus of Computation (Teoria de arrays e de funções não interpretadas) Cap. 9, 11 (complementar)
SMT-LIB
SMT-COMP
Z3 : guide
Z3 internals
Z3 tutorial
notebooks
Decision Procedures (DP) (2nd Ed): Cap. 11.1-11.5, 4.1-4.4, 7.1-7.3
The Calculus of Computation (Teoria de arrays e de funções não interpretadas) Cap. 9, 11 (complementar)
SMT-LIB
SMT-COMP
Z3 : guide
Z3 internals
Z3 tutorial
notebooks
Exercícios:
- Ver os exemplos nos notebooks
- Seguir os tutoriais em:
https://ericpony.github.io/z3py-tutorial/guide-examples.htm
- Ver os exemplos nos notebooks
- Seguir os tutoriais em:
https://ericpony.github.io/z3py-tutorial/guide-examples.htm
Introdução ao demonstrador interactivo Coq usando tipos simples IPC(->). Tipos: Prop e Set. Táticas: intro, apply e assumption.
O interface coqide. 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.
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
O interface coqide. 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.
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