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).
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Narkawicz, Anthony; Muñoz, César; Dutle, Aaron: Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems (2015)
- Rebiha, Rachid; Moura, Arnaldo V.; Matringe, Nadir: Generating invariants for non-linear hybrid systems (2015)
- Larraz, Daniel; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: Minimal-model-guided approaches to solving polynomial constraints and extensions (2014)
- Gao, Sicun; Kong, Soonho; Clarke, Edmund M.: Dreal: an SMT solver for nonlinear theories over the reals (2013)
Further publications can be found at: http://dreal.cs.cmu.edu/publications.html