Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach

Luan V. Nguyen, Wesam Haddad, Taylor T. Johnson

Satisfiability Modulo Theories (SMT) solvers have been successfully applied to solve many problems in formal verification such as bounded model checking (BMC) for many classes of s…