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 δ -complete decision procedures: It returns either unsat or δ -sat on input formulas, where δ is a numerical error bound specified by the user. dReal also produces certificates of correctness for both δ -sat (a solution) and unsat answers (a proof of unsatisfiability).

References in zbMATH (referenced in 30 articles , 1 standard article )

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

1 2 next

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Luteberget, Bjørnar; Claessen, Koen; Johansen, Christian; Steffen, Martin: SAT modulo discrete event simulation applied to railway design capacity analysis (2021)
  3. Beica, Andreea; Feret, Jérôme; Petrov, Tatjana: Tropical abstraction of biochemical reaction networks with guarantees (2020)
  4. Bartholomew, Michael; Lee, Joohyung: First-order stable model semantics with intensional functions (2019)
  5. 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)
  6. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  7. Roux, Pierre; Iguernlala, Mohamed; Conchon, Sylvain: A non-linear arithmetic procedure for control-command software verification (2018)
  8. Roux, Pierre; Voronin, Yuen-Lam; Sankaranarayanan, Sriram: Validating numerical semidefinite programming solvers for polynomial invariants (2018)
  9. Zeljić, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp: Exploring approximations for floating-point arithmetic using uppsat (2018)
  10. Andrea Callia D’Iddio, Michael Huth: Manyopt: An Extensible Tool for Mixed, Non-Linear Optimization Through SMT Solving (2017) arXiv
  11. Chiang, Wei-Fan; Baranowski, Mark; Briggs, Ian; Solovyev, Alexey; Gopalakrishnan, Ganesh; Rakamarić, Zvonimir: Rigorous floating-point mixed-precision tuning (2017)
  12. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF (2017)
  13. Dai, Liyun; Gan, Ting; Xia, Bican; Zhan, Naijun: Barrier certificates revisited (2017)
  14. Djaballah, Adel; Chapoutot, Alexandre; Kieffer, Michel; Bouissou, Olivier: Construction of parametric barrier functions for dynamical systems using interval analysis (2017)
  15. Magron, Victor; Constantinides, George; Donaldson, Alastair: Certified roundoff error bounds using semidefinite programming (2017)
  16. 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)
  17. Shoukry, Yasser; Nuzzo, Pierluigi; Sangiovanni-Vincentelli, Alberto L.; Seshia, Sanjit A.; Pappas, George J.; Tabuada, Paulo: SMC: satisfiability modulo convex optimization (2017)
  18. Tung, Vu Xuan; Khanh, To Van; Ogawa, Mizuhito: raSAT: an SMT solver for polynomial constraints (2017)
  19. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
  20. Mitsch, Stefan; Platzer, André: ModelPlex: verified runtime validation of verified cyber-physical system models (2016)

1 2 next

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