Satisfiability Modulo ODEs

TL;DR

This paper introduces scalable delta-complete algorithms for SMT problems involving ordinary differential equations, enhancing formal verification of hybrid systems and embedded software.

Contribution

It develops novel delta-complete algorithms for existential and exists-forall SMT formulas with ODEs, implemented in the open-source solver dReal.

Findings

Algorithms demonstrate scalability on benchmarks with hundreds of nonlinear ODEs.

Effective handling of purely existential and restricted exists-forall SMT formulas.

Open-source implementation available for practical use.

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.