Exercises Hoare

1 Outubro 2025, 18:30 • Antónia Lopes

Exercises1 (Hoare): 5, 6, 9, 10, 7

---

Mechanising Deductive Verification

1 Outubro 2025, 16:30 • Antónia Lopes

• 
  
  • The syntatic incompleteness of arithmetic and its consequences for the mechanisation of Deductive Program Verification
  • Introduction to Dafny 
    • simple methods and functions
    • specification primitives: assume, assert, invariant, decreases
    • proof-assistant and lemmas
    • write Hoare triples in Dafny
  • Dafny architecture
    • Verification conditions
    • Bounded programs
    • Weakest precondition calculus
    • Generation of verification conditions for bounded programs with WLP calculus
    • Checking verification conditions with a SMT solver

---

Exercises Hoare

24 Setembro 2025, 18:30 • Antónia Lopes

Exercises1 (Hoare): 1.2 p, w 1.4 a,b,c

---

Deductive Software Verification II

24 Setembro 2025, 16:30 • Antónia Lopes

• 
  

• • Hoare logic (cont'd):
    • Proving termination
    • Soundness and completeness
    • Pros & Cons
  • More Logic Recap:
    • Proof system vs deductive system
    • 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 and its consequences for the mechanisation of Deductive Program Verification

---

Exercises Hoare

17 Setembro 2025, 18:30 • Antónia Lopes

Exercises1(Hoare): 1 a, c, e, h; 2 c, f, i, k.

---