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

职业：子句生成：并行符号模型检查的新视角

• 批准号: 0952617
• 负责人: Aaron Bradley
• 金额: $ 49.5万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-01-01 至 2012-02-29
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0952617&HistoricalAwards=false
• 关键词: CAREER; Clause; Generation; New; Perspective

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.

符号有限状态模型检验是一种分析计算系统性质的技术。这个项目重新思考符号模型检查，以实现多核和网络计算机上的可扩展性能。目前尝试并行化模型检查使用标准的算法和技术，但这个项目采取了一种新的方法，其中并行线程共享布尔子句，这是最终证明的引理。 据推测，这样的条款代表了适当的量子共享信息的并行化：既不简单，导致过度的通信，也不复杂，导致线程重复工作。 如果假设是正确的，实现将实现与计算机核心数量的近线性缩放。 该工作还研究了验证属性的正确性与检查属性的反例之间的权衡，探索性能的影响的tradeoffs.Symbolic模型检查有广泛的应用领域，从验证时序电路和安全协议，分析生物过程。 模型检验的进步允许人们分析越来越复杂的系统。 该项目将通过制定提高劳动力逻辑能力的课程，以及为中学生编写关于计算思维的教材，将研究与教育结合起来。