DocumentCode
651314
Title
Satisfiability modulo ODEs
Author
Sicun Gao ; Soonho Kong ; Clarke, Edmund M.
Author_Institution
Comput. Sci. Dept., Carnegie Mellon Univ., Pittsburgh, PA, USA
fYear
2013
fDate
20-23 Oct. 2013
Firstpage
105
Lastpage
112
Abstract
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 δ-complete algorithms for SMT formulas that are purely existentially quantified, as well as ∃∀-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.
Keywords
computability; differential equations; formal verification; δ-complete algorithms; ∃∀-formulas; SMT benchmarks; SMT problems; embedded software; formal verification; open-source solver dReal; ordinary differential equations; realistic hybrid systems; satisfiability modulo ODE; universal quantification; Algorithm design and analysis; Benchmark testing; Encoding; Iterative closest point algorithm; Radio frequency; Standards; Time-domain analysis;
fLanguage
English
Publisher
ieee
Conference_Titel
Formal Methods in Computer-Aided Design (FMCAD), 2013
Conference_Location
Portland, OR
Type
conf
DOI
10.1109/FMCAD.2013.6679398
Filename
6679398
Link To Document