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.