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