Mechanising Deductive Verification
19 Outubro 2022, 16:30 • Antónia Lopes
Mechanising Deductive Verification
- Introduction to Dafny
- methods, functions and lemmas
- Hoare calculus in Dafny
- Weakest precondition calculus
- Dafny architecture
- Verification conditions
- Bounded programs
- The use of a SMT solver