Sumários

Exercises Hoare Calculus

27 Setembro 2023, 18:30 Antónia Lopes

  • Exercises1: 2 (h), (j), (l. Deductive proofs for two more complex programs: downwards sum and power.


Deductive Software Verification I

27 Setembro 2023, 16:30 Antónia Lopes

  • Logic recap:
    • Syntax, Semantics
    • Validity, Satisfiability
    • Proof System 
    • Examples: propositional and first-order logic
  • Hoare logic:
    • Hoare triples 
    • Deductive system for partial correctness
    • Proofs represented as trees and annotated programs


Required tools for the course

20 Setembro 2023, 18:30 Antónia Lopes

  • Quick tour of the tools required for the course assignments  


Introduction

20 Setembro 2023, 16:30 Antónia Lopes

  • Synopsis, including objectives, bibliography, effort required to complete the course, and grading
  • Overview of the major topics covered in the course