Hybrid systems are characterized by non-trivial interactions between discrete (digital) and continuous (analog) components. A typical example is a digital controller in an analog environment, e.g., a micro-controller in a car or plane. The correct behavior of the system depends critically on the interaction between the controller and its environment. The purpose of this project is to develop algorithms that automatically determine the correctness of such systems using a state exploration technique called Model Checking.
Although several methods for hybrid system model checking have been proposed and implemented in research tools, the applications reported in the literature are usually handcrafted examples carefully constructed to illustrate the concepts. The goals of this project are to: (i) develop a new graph-based technique for hybrid system model checking; (ii) develop new methods that combine the power of SAT solvers - which have been successful in hardware verification - with tools for handling continuous variables; and (iii) perform extensive empirical studies to evaluate the relative strengths of several methods for hybrid system verification, including the ones developed in this project, using a set of new extensible benchmark problems (A navigation problem for autonomous vehicles, a leak detection algorithm for pressurized gas pipelines, etc.)
