- SAT-solvers: DPLL and CDCL.
- Satisfiability modulo various logical theories including bitvectors, arrays, integers, reals, rationals, strings,
- Combining Decision Procedures: Nelson-Oppen Method
- Reasoning about quantifiers
Applications to program verification
- Modeling programs in first-order theories
- Reasoning about programs via constraint-solving problem
- Synthesis of invariants and ranking function: interpolation, computational learning, IC3, etc.
- Interactive theorem proving