An abstract interpretation of DPLL(T)

DPLL(T) is a central algorithm for Satisfiability Modulo Theories (SMT) solvers. The algorithm combines results of reasoning about the Boolean structure of a formula with reasoning about conjunctions of theory facts to decide satisfiability. This architecture enables modern solvers to combine the pe...

Full beskrivning

Bibliografiska uppgifter
Huvudupphovsmän: Brain, M, D'Silva, V, Haller, L, Griggio, A, Kroening, D
Övriga upphovsmän: Giacobazzi, R
Materialtyp: Conference item
Publicerad: Springer 2013