This award provides support for a two year research project between Professor Edmund Clarke, School of Computer Science, Carnegie Mellon University, and Professor Hiromi Hiraishi, Department of Information Science, Kyoto University, Japan. The aim of the project is to investigate formal verification methods for finite state systems. These systems arise naturally in the design of computer software and communication protocols, and their correctness is likely to become an important issue in the future. Recent work has shown that finite systems can often be verified automatically by constructing and analyzing state-graph models of system behavior. However these methods rely on decision algorithms which explicitly construct the state-graph model and because the number of states in a model may grow exponentially with the number of concurrently executing components, the complexity of systems that can be verified has been limited. This research will focus on new techniques which avoid this problem, so that formal verification can be applied to systems of realistic complexity. A number of alternative techniques have been proposed. One example is to exploit the hierarchical structure of the circuit in the verification process. Each individual component may be verified separately and the results combined to infer properties of the global behavior of the system. A second approach is to implement parallel algorithms that will run on supercomputers. Both the US and Japanese researchers involved in this project have been developing techniques for detecting these design errors and recent research by both provides strong evidence that it is possible to develop practical tools for this purpose. The research skills of the two researchers are complementary and each country has much to learn from the other about ways of dealing with this problem. If successful this project should lead to new techniques for automatic design verification of finite state systems.
