Temporal Logic, Hardware Verification, and Automatic Theorem Proving

点击翻译按钮获取中文摘要

This work comprises several research projects in logics of programs and program verification. All of the projects are directed towards providing tools that will make automatic verification feasible for a wider class of programs. The first three projects involve an approach to verifying finite state concurrent systems called temporal logic model checking. This procedure will determine if a finite-state concurrent system satisfies its specification in a propositional temporal logic by methodically searching the global state graph generated by the concurrent system. It has been used successfully to find subtle errors in published designs of tricky self-timed circuits. The first project is to develop ways of handling the state explosion problem that may occur with this type of verification. Another project is to extend the temporal logic and its verification procedure to allow operators defined by automata on infinite tapes. This is of practical importance since a frequent criticism of temporal logic is its expressive power compared to automata. The third project involves actually using model checking techniques for the automatic verification of hardware controllers. The main problem in this case is to develop methods of extracting state machines from circuits under realistic timing models. The last project is the development of a parallel resolution theorem prover to run on Sequent and Encore multiprocessors. It is already well underway. Since interest primarily in problems caused by concurrency, one can use a fairly simple theorem proving strategy based on linear resolution/model elimination. Clauses are maintained according to some heuristic function in a heap data structure that permits parallel inserts and deletions. A prototype implementation of the full system should be running in the next few months. Experiments with other ways of organizing the theorem prover and with more complicated theorem proving strategies will follow.