Skip to content
scrambled
Programming Language Theory Concept

SMT solver

Books JourneyProgramming Language Theory Statuslearning Tags
  • formal system
  • logic
  • program analysis

A Decision procedure that determines satisfiability of formulas in first-order logic with theories (like arithmetic, arrays, bit-vectors), extending SAT solver to richer domains.

A decision procedure that determines satisfiability of formulas in first-order logic with theories (like arithmetic, arrays, bit-vectors), extending SAT to richer domains.