Model Checking Algorithms for Protocols and Hybrid Systems

We focus on the design of model checking algorithms that exploit the statistical structure of the problem at hand. For example, this is done on the system source code in [LICS 1995, FM-Trends 1998] and by exploiting transition locality of the system transition graph in [CHARME 2001]. Furthermore, always exploiting transition locality, fast disk based model checking algorithms have been designed and implemented in [FMCAD 2002, HSCC 2003, CHARME 2003, STTT 2004, FMCAD 2004, CIMCA 2005]. A disk based probabilistic model checker has also been designed in [APSEC 2001]. In [FM-Trends 1998] we investigated model checking algorithms for logics with actions. In [HSCC 2007] we investigated SAT based bounded model checking of hybrid systems. In [APSEC 2007] we investigated disk based algorithms for SAT based bounded model checking of software systems.