Deductive Software Verification II

7 Outubro 2016, 16:30 Antónia Lopes

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