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

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

1 2 next

  1. Bartholomew, Michael; Lee, Joohyung: First-order stable model semantics with intensional functions (2019)
  2. Islam, Md. Ariful; Cleaveland, Rance; Fenton, Flavio H.; Grosu, Radu; Jones, Paul L.; Smolka, Scott A.: Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans (2019)
  3. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  4. Roux, Pierre; Iguernlala, Mohamed; Conchon, Sylvain: A non-linear arithmetic procedure for control-command software verification (2018)
  5. Roux, Pierre; Voronin, Yuen-Lam; Sankaranarayanan, Sriram: Validating numerical semidefinite programming solvers for polynomial invariants (2018)
  6. Zeljić, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp: Exploring approximations for floating-point arithmetic using uppsat (2018)
  7. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  8. Chiang, Wei-Fan; Baranowski, Mark; Briggs, Ian; Solovyev, Alexey; Gopalakrishnan, Ganesh; Rakamarić, Zvonimir: Rigorous floating-point mixed-precision tuning (2017)
  9. Dai, Liyun; Gan, Ting; Xia, Bican; Zhan, Naijun: Barrier certificates revisited (2017)
  10. Djaballah, Adel; Chapoutot, Alexandre; Kieffer, Michel; Bouissou, Olivier: Construction of parametric barrier functions for dynamical systems using interval analysis (2017)
  11. Magron, Victor; Constantinides, George; Donaldson, Alastair: Certified roundoff error bounds using semidefinite programming (2017)
  12. 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)
  13. Shoukry, Yasser; Nuzzo, Pierluigi; Sangiovanni-Vincentelli, Alberto L.; Seshia, Sanjit A.; Pappas, George J.; Tabuada, Paulo: SMC: satisfiability modulo convex optimization (2017)
  14. Tung, Vu Xuan; Khanh, To Van; Ogawa, Mizuhito: raSAT: an SMT solver for polynomial constraints (2017)
  15. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
  16. Mitsch, Stefan; Platzer, André: ModelPlex: verified runtime validation of verified cyber-physical system models (2016)
  17. Tiwari, Ashish; Lincoln, Patrick: A search-based procedure for nonlinear real arithmetic (2016)
  18. Tung, Vu Xuan; Van Khanh, To; Ogawa, Mizuhito: raSAT: an SMT solver for polynomial constraints (2016)
  19. Bae, Kyungmin; Ölveczky, Peter Csaba: Hybrid multirate PALS (2015)
  20. 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)

1 2 next


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