This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
course:smt [2017/09/04 16:47] mht208 [Part I] |
course:smt [2017/09/04 16:47] (current) mht208 [Part II] |
||
---|---|---|---|
Line 9: | Line 9: | ||
We show how to verify if a program satisfies a specification with Hoare logic and how to generate verification conditions with weakest preconditions. Besides backward reasoning, we also show how to verify a program in a forward manner. | We show how to verify if a program satisfies a specification with Hoare logic and how to generate verification conditions with weakest preconditions. Besides backward reasoning, we also show how to verify a program in a forward manner. | ||
- | {{ :course:03_verification.pdf |Verification}}, {{ :course:04_verify25519.pdf |Cryptographic Software}}{{ :course:verification_exercises.pdf |Exercises}} | + | {{ :course:03_verification.pdf |Verification}}, {{ :course:04_verify25519.pdf |Cryptographic Software}}{{ :course:verification_exercises.pdf |Exercises}}, {{ :course:verification_exercises_sol.pdf |Suggested Solutions}} |