Satisfiability Modulo Theories and Its Applications in Software Model Checking


  • 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



en/lecture/smt.txt · Last modified: 2011/06/29 11:55 by yfc