Satisfiability Modulo ODEs
Logic in Computer Science
2013-10-31 v1 Systems and Control
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 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.
Cite
@article{arxiv.1310.8278,
title = {Satisfiability Modulo ODEs},
author = {Sicun Gao and Soonho Kong and Edmund Clarke},
journal= {arXiv preprint arXiv:1310.8278},
year = {2013}
}
Comments
Published in FMCAD 2013