Sumários

Design By Contract

16 Outubro 2019, 18:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Approaches to DBC (Design by Contract)
    • Preconditions and postconditions
    • Blame assignment
  • DBC with Dafny
    • Procedural abstraction
    • Additional specification features
  • Hoare Logic versus Design by Contract
  • Design by Contract in Dafny

Design By Contract

16 Outubro 2019, 16:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Approaches to DBC (Design by Contract)
    • Preconditions and postconditions
    • Blame assignment
  • DBC with Dafny
    • Procedural abstraction
    • Additional specification features
  • Hoare Logic versus Design by Contract
  • Design by Contract in Dafny

Deductive Software Verification III

9 Outubro 2019, 18:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Proving termination
  • Soundness and completeness
  • Pros & cons
  • Compositionality
  • Hoare Logic in Dafny
  • Architecture of Dafny
  • Weakest (Liberal) Preconditions
  • Generation of Verification Conditions

Deductive Software Verification III

9 Outubro 2019, 16:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Proving termination
  • Soundness and completeness
  • Pros & cons
  • Compositionality
  • Hoare Logic in Dafny
  • Architecture of Dafny
  • Weakest (Liberal) Preconditions
  • Generation of Verification Conditions

Deductive Software Verification II

2 Outubro 2019, 18:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Hoare logic