2013/10/30 by Sicun Gao, Gao, Sicun, Soonho Kong +3
Computer Science · #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Numerical Methods and Algorithms #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1310.8278
openalex publication_date 2013/10/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We study SMT problems over the reals containing ordinary differential equations. They are important for formal verification of realistic hybrid systems and embedded software. We develop delta-complete algorithms for SMT formulas that are purely existentially quantified, as well as exists-forall formulas whose universal quantification is restricted to the time variables. We demonstrate scalability of the algorithms, as implemented in our open-source solver dReal, on SMT benchmarks with several hundred nonlinear ODEs and variables.