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 20 articles , 1 standard article )

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

  1. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  2. Chiang, Wei-Fan; Baranowski, Mark; Briggs, Ian; Solovyev, Alexey; Gopalakrishnan, Ganesh; Rakamarić, Zvonimir: Rigorous floating-point mixed-precision tuning (2017)
  3. Dai, Liyun; Gan, Ting; Xia, Bican; Zhan, Naijun: Barrier certificates revisited (2017)
  4. Djaballah, Adel; Chapoutot, Alexandre; Kieffer, Michel; Bouissou, Olivier: Construction of parametric barrier functions for dynamical systems using interval analysis (2017)
  5. Magron, Victor; Constantinides, George; Donaldson, Alastair: Certified roundoff error bounds using semidefinite programming (2017)
  6. Murthy, Abhishek; Islam, Md.Ariful; Smolka, Scott A.; Grosu, Radu: Computing compositional proofs of input-to-output stability using SOS optimization and $\delta$-decidability (2017)
  7. Shoukry, Yasser; Nuzzo, Pierluigi; Sangiovanni-Vincentelli, Alberto L.; Seshia, Sanjit A.; Pappas, George J.; Tabuada, Paulo: SMC: satisfiability modulo convex optimization (2017)
  8. Tung, Vu Xuan; Khanh, To Van; Ogawa, Mizuhito: raSAT: an SMT solver for polynomial constraints (2017)
  9. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
  10. Mitsch, Stefan; Platzer, André: ModelPlex: verified runtime validation of verified cyber-physical system models (2016)
  11. Tiwari, Ashish; Lincoln, Patrick: A search-based procedure for nonlinear real arithmetic (2016)
  12. Tung, Vu Xuan; Van Khanh, To; Ogawa, Mizuhito: raSAT: an SMT solver for polynomial constraints (2016)
  13. Bae, Kyungmin; Ölveczky, Peter Csaba: Hybrid multirate PALS (2015)
  14. 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)
  15. Rebiha, Rachid; Moura, Arnaldo V.; Matringe, Nadir: Generating invariants for non-linear hybrid systems (2015)
  16. Shmarov, Fedor; Zuliani, Paolo: ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems (2015)
  17. Bogomolov, Sergiy; Herrera, Christian; Muñiz, Marco; Westphal, Bernd; Podelski, Andreas: Quasi-dependent variables in hybrid automata (2014)
  18. Larraz, Daniel; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: Minimal-model-guided approaches to solving polynomial constraints and extensions (2014)
  19. Bonacina, Maria Paola (ed.): Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings (2013)
  20. 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