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.

Solved exercises: 1.1 (q), (u), 1.7 (a), 1.8  

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