Lecturer: 陳郁方 Yu-Fang Chen

• Introduction to Satisfiability Modulo Theories (SMT)

1. Software model checking using SMT and tool demonstration
2. Theory of linear arithmetic
3. Theory of equalities and uninterpreted function

• Using SMT for Software Model Checking

1. Predicate Abstraction
2. Counterexample Guided Abstraction Refinement
3. Craig Interpolant in FOL

flolac.pptx flolac.pdf flolac_ii.pptx flolac_ii.pdf

flolac.zip