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
course:smt [2017/08/31 13:35]
mht208 [Part II]
course:smt [2017/09/04 16:47] (current)
mht208 [Part II]
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:​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}}