使用k-归纳法和不变量的模型检验嵌入式C软件（扩展版）
Model Checking Embedded C Software using k-Induction and Invariants (extended version)
摘要：
本文提出了一种基于归纳法的证明方法，将k-归纳法与不变量相结合，对嵌入式C软件中有界循环和无界循环进行模型检验。k-归纳算法由三种情况组成：在基本情况下，我们的目标是找到一个反例，最多有k个循环展开;在正向条件下，我们检查循环是否已经完全展开，以及安全属性P是否在k个展开内的所有状态下都成立;在归纳步骤中，我们检查每当P对k个展开成立时，它在系统的下一个展开后也成立。对于k-归纳算法的每一步，我们使用仿射约束来推断不变量（即，多面体）指定前置和后置条件。实验结果表明，我们的方法可以处理各种各样的安全特性，在典型的嵌入式软件应用程序，从电信，控制系统和医疗设备，我们证明了改进的感应算法的有效性，如果与其他方法相比。
英文摘要：
We present a proof by induction algorithm, which combines k-induction with invariants to model check embedded C software with bounded and unbounded loops. The k-induction algorithm consists of three cases: in the base case, we aim to find a counterexample with up to k loop unwindings; in the forward condition, we check whether loops have been fully unrolled and that the safety property P holds in all states reachable within k unwindings; and in the inductive step, we check that whenever P holds for k unwindings, it also holds after the next unwinding of the system. For each step of the k-induction algorithm, we infer invariants using affine constraints (i.e., polyhedral) to specify pre- and post-conditions. Experimental results show that our approach can handle a wide variety of safety properties in typical embedded software applications from telecommunications, control systems, and medical devices; we demonstrate an improvement of the induction algorithm effectiveness if compared to other approaches.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
