Sumários

Type Specifications I

17 Outubro 2017, 18:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Propery-based specifications in JML
  • Representation-exposing specifications in JML

Type Specifications I

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

  • Propery-based specifications in JML
  • Representation-exposing specifications in JML

Design By Contract

10 Outubro 2017, 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
  • DBC with JML
    • Procedural abstraction and JML assertions
    • Runtime verification

Deductive Software Verification II

3 Outubro 2017, 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 I

26 Setembro 2017, 16:30 • Vasco Manuel Thudichum de Serpa Vasconcelos

  • Proof systems
  • First order logic
  • Partial vs total correctness
  • Hoare logic