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