Explicit Safety Property Strengthening in SAT-based Induction
Explicit Safety Property Strengthening in SAT-based Induction
复制标题
基于 SAT 的归纳中的显式安全属性强化
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
M. Hsiao
中科院分区：
文献类型：
--
作者：
Vishnu C. Vimjam;M. Hsiao
增强财产可以在较早的诱导深度进行伪造/验证。在本文中，我们提出了新的预处理技术，以明确识别给定安全性属性的共同不变，然后将其添加到该属性中以进行更快的验证。首先，我们采用以路径为导向的决策引擎来快速识别几个具有违反该物业的州的州的州。接下来，我们生成一组候选人共变动，并提出一种基于感应的技术，以了解这些候选人的真正共同性。使用分辨率将所有学习过的共变为变为最小化，并添加到原始属性中以加强其。实验表明，证明许多安全性能所需的诱导深度可以通过我们的加强大大降低，从而实现了不仅仅是运行时的数量级改进。
Strengthening a property allows it to be falsified/verified at an earlier induction depth. In this paper, we propose new preprocessing techniques for explicitly identifying co-invariants for a given safety property which are then added to that property for faster verification. First, we employ a path-oriented decision making engine to quickly identify several states which have paths to states violating the property. Next, we generate a set of candidate co-invariants and propose an induction-based technique to learn true co-invariants among those candidates. All the learned co-invariants are minimized using resolution and added to the original property to strengthen it. Experiments show that the induction depth needed to prove many safety properties can be significantly reduced via our strengthening, thereby achieving more than an order of magnitude runtime improvements