Differences

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

Link to this comparison view

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}}