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 9 articles )
Showing results 1 to 9 of 9.
- Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
- Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
- Tiwari, Ashish; Lincoln, Patrick: A search-based procedure for nonlinear real arithmetic (2016)
- 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)
- Shmarov, Fedor; Zuliani, Paolo: ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems (2015)
- Bogomolov, Sergiy; Herrera, Christian; Muñiz, Marco; Westphal, Bernd; Podelski, Andreas: Quasi-dependent variables in hybrid automata (2014)
- 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