Modern Graph Algorithmic Techniques in Formal Verification

One of the most important challenges in computer science is to develop correct systems or write correct programs. Subtle errors in complex systems and large programs lead to many critical errors such as the famous Pentium bug, or explosions of space rockets (such as ESA`s Ariane 5 rocket). The field of computer aided verification develops automated techniques that formally analyze the correctness of systems and help in discovering subtle errors and bugs. In computer aided verification first a mathematical model of the system is created. Usually these mathematical models are extensions of graph models, where vertices represent states of the system, edges represent transitions, and paths represent behaviors of the system. The mathematical model is then analyzed against a specification which describes the desired set of behaviors of the system. Thus in the heart of the automated techniques are algorithms for analysis of graph properties. As systems that are being developed are becoming larger and more complex at a rapid pace, there is a danger that the existing computer aided verification techniques fail to keep up and become very slow. At the same time modern algorithmic techniques have significantly improved graph algorithmic problems in other fields, but are not yet employed in verification. Hence our goal is to use these new algorithmic techniques to speed up graph theoretic problems in computer aided verification in order to allow it to cope with increased complexity and size. Since most computer aided verification techniques use few core graph theoretic algorithms, we will focus on improving them to impact the formal analysis of systems and programs for a wide range of applications. This is also of theoretical interest as for these problems there are large gaps between the current best known algorithms and the lower bounds. We will focus on the following two modern algorithmic techniques to improve the running time of algorithms of these problems. 1. Dynamic graph algorithmic techniques: Many algorithms in computer aided verification use repeated computation on similar graphs, yet none of the algorithms use data structures developed for dynamic graph problems. We will explore the development of new data structures and techniques for dynamic graph problems to obtain better algorithms. 2. Randomized techniques: Many connectivity-related graph problems can be solved more efficiently with randomization, yet few algorithms in computer aided verification use any randomization. We will study how randomization can be used to design faster algorithms. We will also develop symbolic versions of our algorithms and present efficient implementations of them in a research prototype to demonstrate the practical feasibility of our algorithms.

One key challenge in computer science is to develop correct systems or write correct programs. Subtle errors in complex systems and large programs lead to many critical errors such as the famous Pentium bug, or explosions of space rockets (such as ESA's Ariane 5 rocket). The field of computer aided verification develops automated techniques that formally analyze the correctness of systems and help in discovering subtle errors and bugs. In computer aided verification first a mathematical model of the system is created. Usually these mathematical models are extensions of graph models, where vertices represent states of the system, edges represent transitions, and paths represent behaviors of the system. The mathematical model is then analyzed against a specification which describes the desired set of behaviors of the system. Thus in the heart of the automated techniques are algorithms for analysis of graph properties. As systems that are being developed are becoming larger and more complex at a rapid pace, there is a danger that the existing computer aided verification techniques fail to keep up and become very slow. At the same time modern algorithmic techniques have significantly improved graph algorithmic problems in other fields, but are not yet employed in verification. In this project, we used modern graph algorithmic techniques to obtain faster algorithms for several classical problems in computer aided verification, and in some cases, we broke long-standing algorithmic barrier for many basic problems. We also developed symbolic versions of our algorithms and developed prototype implementations to show the feasibility of our methods to robotics applications.