Sumários
Mechanising Deductive Verification
19 Outubro 2022, 16:30 • Antónia Lopes
Mechanising Deductive Verification
- Introduction to Dafny
- methods, functions and lemmas
- Hoare calculus in Dafny
- Weakest precondition calculus
- Dafny architecture
- Verification conditions
- Bounded programs
- The use of a SMT solver
Hoare Logic
12 Outubro 2022, 18:30 • Antónia Lopes
Making simple proofs in Hoare Calculus. Clues on how to find loop invariants. Understand soundness and completeness.
Hoare Logic (cont'd(
12 Outubro 2022, 16:30 • Antónia Lopes
- Deductive Software Verification II
- Proof System (cont'd):
- Soundness and Completeness
- Formal theory
- Consistency (syntactically soundness)
- Syntatic Completeness
- Examples of first-order theories
- Theory of equality
- Theory of Presburger arithmetic
- Theory of Peano arithmetic
- The syntatic incompleteness of arithmetic
- Hoare logic (cont'd):
- Proving termination
- Soundness and completeness
- Pros & Cons
Deductive verification with Hoare Logic
28 Setembro 2022, 18:30 • Antónia Lopes
A deductive proof of the partial correctness of a program that calculates the power of a number.
Deductive Software Verification
28 Setembro 2022, 16:30 • Antónia Lopes
- Logic
- Syntax, Semantics
- Validity, Satisfiability
- Proof System
- Examples: propositional and first-order logic
- Hoare logic:
- Program analysis as a validity checking problem
- Partial vs total correctness
- Deductive system for partial correctness