Sciweavers

FORMATS
2010
Springer
13 years 9 months ago
Natural Domain SMT: A Preliminary Assessment
SMT solvers have traditionally been based on the DPLL(T) algorithm, where the driving force behind the procedure is a DPLL search over truth valuations. This traditional framework ...
Scott Cotton
ENTCS
2008
64views more  ENTCS 2008»
13 years 11 months ago
Model-based Theory Combination
Traditional methods for combining theory solvers rely on capabilities of the solvers to produce all implied equalities or a pre-processing step that introduces additional literals...
Leonardo Mendonça de Moura, Nikolaj Bj&osla...
CAV
2008
Springer
121views Hardware» more  CAV 2008»
14 years 1 months ago
The Barcelogic SMT Solver
This is the first system description of the Barcelogic SMT solver, which implements all techniques that our group has been developing over the last four years as well as state-of-t...
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras...