Sumários

Exercise about Hoare Logic and Dafny

9 Outubro 2024, 18:30 • Antónia Lopes

  • Exercises2 (Dafny-Hoare): 2,3,4,8

Mechanising Deductive Verification (cont'd)

9 Outubro 2024, 16:30 • Antónia Lopes

  • Mechanising Deductive Verification (cont'd)
    • 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
  • Introduction to design by contract (DbC)
  • Contracts for procedural abstractions
    • pre- and postconditions
    • blame assignment
    • Hoare triples vs contracts
  • Compositional reasonig
  • DbC for procedural abstractions in Dafny
    • More about methods and functions

Exercises about Hoare Logic

2 Outubro 2024, 18:30 • Antónia Lopes

Mechanising Deductive Verification

2 Outubro 2024, 16:30 • Antónia Lopes

  • Mechanising Deductive  Verification 
    • 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
    • Introduction to Dafny 
      • simple methods and functions
      • specification primitives: assume, assert, invariant, decreases
      • proof-assistant and lemmas
      • write Hoare triples in Dafny

Deductive Software Verification I

25 Setembro 2024, 18:30 • Antónia Lopes

Exercises 1.1 a, c, e, h; 1.2 c, f, i, k; 1.4 a, b.