Here we only list papers that explain the core techniques in dReal.

• Proof Generation from Delta-Decisions.
  Sicun Gao, Soonho Kong, and Edmund Clarke
  In SYNASC (International Conference on Symbolic and Numerical Algorithms for Scientific Computing) 2014

• Satisfiability Modulo ODEs.
  Sicun Gao, Soonho Kong, and Edmund Clarke
  In FMCAD (Formal Methods in Computer-Aided Design) 2013 [pdf]

• dReal: An SMT Solver for Nonlinear Theories of the Reals (Tool Paper).
  Sicun Gao, Soonho Kong, and Edmund Clarke
  In CADE (Conference on Automated Deduction) 2013 [pdf]

• Computable Analysis, Decision Procedures, and Hybrid Automata: A New Framework for the Formal Verification of Cyber-Physical Systems.
  Sicun Gao
  PhD Thesis, Carnegie Mellon University, 2012

• Delta-Complete Decision Procedures for Satisfiability over the Reals.
  Sicun Gao, Jeremy Avigad, and Edmund Clarke
  In IJCAR (International Joint Conference on Automated Reasoning) 2012 [arXiv]

• Delta-Decidability over the Reals.
  Sicun Gao, Jeremy Avigad, and Edmund Clarke
  In LICS (Logic in Computer Science) 2012 [arXiv]