CAREER: Clause Generation: A New Perspective on Parallel Symbolic Model Checking

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

Symbolic finite-state model checking is a technique for analyzing properties of computational systems. This project rethinks symbolic model checking to achieve scalable performance on multi-core and networked computers. Current attempts to parallelize model checking use standard algorithms and techniques, but this project takes a new approach in which parallel threads share Boolean clauses, which are lemmas of the final proof. It is hypothesized that such clauses represent the appropriate quantum of shared information for parallelization: neither so simple as to cause excessive communication, nor so complex as to cause threads to duplicate work. If the hypothesis is correct, implementations will achieve near-linear scaling with the number of computer cores. The work also investigates the tradeoffs between verifying correctness of properties versus checking properties for counterexamples, exploring performance implications of the tradeoffs.Symbolic model checking has applications in a wide range of areas, from verifying sequential circuits and security protocols to analyzing biological processes. Advances in model checking allow one to analyze systems of increasingly higher complexity. The project will integrate research and education by developing curriculum that increases the workforce's proficiency in logic, as well as develop educational material on computational thinking for secondary school students.