A procedure, called temporal logic model checking, for automatic verification of concurrent programs has been developed. This procedure determines if a collection of finite-state processes satisfies its specification in a propositional temporal logic by methodically searching the global state graph determined by the processes. The first part of this project deals with temporal logic model checking and how it can be extended to verify hardware controllers, cache coherency protocols, and real-time programs. In particular, new techniques (various methods for compositional model checking, alternative state space representations using binary decision graphs and partial orders, etc.) will be developed to extend the size of the finite state programs that can be handled using this technique. The second part of this project deals with parallel theorem proving and symbolic computation. A parallel resolution theorem prover called Parthenon has been built. In this project, a number of important algorithms for theorem proving and symbolic computation will be implemented on different types of multiprocessors.
