# dReal

Dreal: an SMT solver for nonlinear theories over the reals We describe the open-source tool dReal, an SMT solver for nonlinear formulas over the reals. The tool can handle various nonlinear real functions such as polynomials, trigonometric functions, exponential functions, etc. dReal implements the framework of $delta$-complete decision procedures: It returns either unsat or $delta$-sat on input formulas, where $delta$ is a numerical error bound specified by the user. dReal also produces certificates of correctness for both $delta$-sat (a solution) and unsat answers (a proof of unsatisfiability).

## References in zbMATH (referenced in 28 articles , 1 standard article )

Showing results 1 to 20 of 28.
Sorted by year (citations)

## 1 2next

Further publications can be found at: http://dreal.cs.cmu.edu/publications.html