Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods

Aiming at automatic verification and analysis techniques for hybrid systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art enclosure method for ODEs, and with bracketing systems which exploit …