Trace:

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||

course:smt [2017/08/31 13:21] mht208 |
course:smt [2017/09/04 16:47] mht208 [Part I] |
||
---|---|---|---|

Line 3: | Line 3: | ||

We introduce some first-order theories in this lecture. Some decidable fragments of first-order theories and decision procedures of satisfiability are also introduced. We will learn how to reduce a problem to a problem in satisfiability modulo theories (SMT) and how to use an SMT solver to solve it. | We introduce some first-order theories in this lecture. Some decidable fragments of first-order theories and decision procedures of satisfiability are also introduced. We will learn how to reduce a problem to a problem in satisfiability modulo theories (SMT) and how to use an SMT solver to solve it. | ||

- | {{ :course:01_smt.pdf |SMT}}, {{ :course:02_euf.pdf |Decision Procedures}}, {{ :course:smt_exercises.pdf | Exercises}} | + | {{ :course:01_smt.pdf |SMT}}, {{ :course:02_euf.pdf |Decision Procedures}}, {{ :course:smt_exercises.pdf | Exercises}}, {{ :course:smt_exercises_sol.pdf |Suggested Solutions}} |

===== Part II ===== | ===== 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:verification_exercises.pdf |Exercises}} | + | {{ :course:03_verification.pdf |Verification}}, {{ :course:04_verify25519.pdf |Cryptographic Software}}{{ :course:verification_exercises.pdf |Exercises}} |

Last modified: 2017/09/04 16:47

Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Share Alike 4.0 International