Flexible SAT-based framework for incremental bounded upgrade checking
Flexible SAT-based framework for incremental bounded upgrade checking
复制标题
基于灵活的 SAT 框架，用于增量有界升级检查
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
N. Sharygina
中科院分区：
文献类型：
--
作者：
Grigory Fedyukovich;Ondřej Šerý;N. Sharygina
软件在其生命周期中会经历无数微小的变化。程序的每一次演化转换都被期望保持重要的正确性和安全性，特别是由软件模型检查工具确认。然而，为程序的每个新版本重复整个模型检查可能非常耗费资源和时间。作为一种可能的解决方案，我们建议通过重用前一个程序版本的有界模型检查来对新程序版本进行增量分析。我们的方法通过使用克雷格插值导出的函数摘要来保持有界程序行为的过度逼近。对于每个新版本，这些摘要用于定位模型检查的范围。这种方法的一个好处是，升级检查的成本取决于两个版本之间的更改影响。如果变更影响相对较小，那么增量检查的性能可以大大超过从头开始检查新程序版本的模型。我们在基于sat的C语言有界模型检查器eVolCheck的范围内实现了该方法。eVolCheck的评估证实，增量变化可以有效地验证不同类别的工业方案。
Software undergoes a myriad of minor changes along its lifecycle. Each evolved transformation of a program is expected to preserve important correctness and security properties, in particular confirmed by a software model checking tool. However, it may be extremely resource- and time-consuming to repeat entire model checking for each new version of the program. As a possible solution to this problem, we propose to conduct incremental analysis of a new program version by reusing efforts of bounded model checking of the previous program version. Our approach maintains over-approximations of the bounded program behaviors by means of function summaries derived using Craig interpolation. For each new version, these summaries are used to localize the scope of model checking. A benefit of this approach is that the cost of the upgrade checking depends on the change impact between the two versions. If the change impact is relatively small, then the incremental check can drastically outperform the model checking the new program version from scratch. We implemented the approach in scope of the SAT-based bounded model checker for C, eVolCheck. The evaluation of eVolCheck confirms that incremental changes can be verified efficiently for different classes of industrial programs.