# Satisfiability Modulo ODEs

arXiv: https://arxiv.org/abs/1310.8278 · HTML: https://mlsanity.com/paper/1310.8278/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Oct 2013.

## Built on by (most cited first, 3 of 3)

- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [First-Order Stable Model Semantics with Intensional Functions](https://mlsanity.com/paper/2307.10225/) (2023)
- [Robustness Analysis of Continuous-Depth Models with Lagrangian Techniques](https://mlsanity.com/paper/2308.12192/) (2023)

## Abstract (arXiv)

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.