无界软件模型检验与增量SAT求解
Unbounded Software Model Checking with Incremental SAT-Solving
摘要：
提出了一种基于增量SAT求解的无界软件模型检验方法，用于发现C语言程序中的错误。而不是使用传统的假设为基础的API增量SAT求解器，我们使用的DimSpec格式，用于SAT的自动规划。DimSpec公式由四个CNF公式组成，分别表示过渡系统的初始状态、目标状态和中间状态以及每对相邻状态之间的关系。我们提出了一种新的工具，称为LLUMC编码的存在下，在C程序中的某些错误到一个DimSpec公式，它可以解决增量SAT为基础的DimSpec求解器或IC3算法不变检查。我们评估的情况下，基于SAT的模型检验的增量SAT求解和IC3算法的方法。我们表明，我们的编码还覆盖了大型和无限循环，同时仍然保持了可行的时间性能，从而扩展了有界模型检查器的功能。此外，我们证明了我们的方法提供了机会，通过利用并行SAT求解生成运行时优化。
英文摘要：
This paper describes a novel unbounded software model checking approach to find errors in programs written in the C language based on incremental SAT-solving. Instead of using the traditional assumption based API to incremental SAT solvers we use the DimSpec format that is used in SAT based automated planning. A DimSpec formula consists of four CNF formulas representing the initial, goal and intermediate states and the relations between each pair of neighboring states of a transition system. We present a new tool called LLUMC which encodes the presence of certain errors in a C program into a DimSpec formula, which can be solved by either an incremental SAT-based DimSpec solver or the IC3 algorithm for invariant checking. We evaluate the approach in the context of SAT-based model checking for both the incremental SAT-solving and the IC3 algorithm. We show that our encoding expands the functionality of bounded model checkers by also covering large and infinite loops, while still maintaining a feasible time performance. Furthermore, we demonstrate that our approach offers the opportunity to generate runtime-optimizations by utilizing parallel SAT-solving.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
