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.