# Differences

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

 course:smt [2017/08/31 13:21]mht208 course:smt [2017/09/04 16:47]mht208 [Part I] Both sides previous revision Previous revision 2017/09/04 16:47 mht208 [Part II] 2017/09/04 16:47 mht208 [Part I] 2017/08/31 13:35 mht208 [Part II] 2017/08/31 13:21 mht208 2017/08/30 13:17 mht208 created Next revision Previous revision 2017/09/04 16:47 mht208 [Part II] 2017/09/04 16:47 mht208 [Part I] 2017/08/31 13:35 mht208 [Part II] 2017/08/31 13:21 mht208 2017/08/30 13:17 mht208 created Last revision Both sides next revision 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}}