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...

ver descrição completa

Detalhes bibliográficos
Principais autores: Brain, M, D'Silva, V, Haller, L, Griggio, A, Kroening, D
Outros Autores: Giacobazzi, R
Formato: Conference item
Publicado em: Springer 2013