Model Checking Algorithms for Protocols and Hybrid Systems

Details
Category: Research
Last Updated on Monday, 26 November 2012 16:32

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.