模型检查是形式化方法中一种基于数学和逻辑的验证技术，用于检查系统或软件是否满足特定规范。该方法在高可信系统，如航空航天、铁路信号系统、通信协议和硬件设计等领域得到广泛应用。模型检查方法的核心是将系统形式化地建模为状态模型，并运用算法来验证系统性质。然而，对于大型系统，由于状态空间爆炸问题，模型检查可能会面临计算复杂性的挑战。最近，软件工程学院博士研究生夏晔川在模型检查算法方面取得了重要的研究进展。

夏晔川与合作者针对状态空间爆炸问题，基于模型检查算法理论提出了一种优化基于SAT求解器的模型检查算法性能的方法，相关论文Searching for i-Good Lemmas to Accelerate Safety Model Checking在形式化验证领域国际顶级会议International Conference on Computer Aided Verification（CAV 2023）上发表，并由夏晔川作为第一作者进行报告。

该工作提出了一种简单但十分有效的提升有限状态空间安全性质模型检查算法性能的方法。在安全性质模型检查算法当中，IC3/PDR因为其完备性以及有效性成为目前最杰出的一种算法。在IC3/PDR中，引理构造对于算法的性能十分关键，然而由于引理主要来自于SAT求解器提供的结果，引理构造带来的性能差异在先前的工作中没有得到研究。而在该工作中，夏晔川与其合作者基于对算法理论的深入研究，定义了一种可以加速算法收敛的引理特征，并设计了帮助算法搜索该种引理的策略，有效地提升了模型检查算法的性能。

对IC3/PDR构造的引理序列进行可视化，左右为不同的引理序列构造。算法在左侧序列上无法收敛，而可以在右侧序列上收敛

除了IC3/PDR外，该工作还涉及另一种模型检查算法互补近似可达（CAR）的评估，该算法由夏晔川导师、学院青年研究员李建文提出。将优化方法应用于开源的IC3和CAR工具后，它们的性能能够优于Berkeley大学开发的模型检查工具ABC。此外，该工作与开发了著名模型检查工具集nuXmv的小组合作，将优化方法运用于该商业工具，该全新的优化策略使得高度优化的nuXmv的性能也得到了提升。

不同工具上实现的IC3和CAR在运用该优化后的性能差异

近五年来，由李建文带领的研究小组已在模型检查算法方向发表多篇文章，更多相关研究工作可参考https://lijwen2748.github.io/tools/2023-07-17-simplecar。

图文由论文作者提供

编辑丨陈励

审核丨曹桂涛