论文标题
正确的非确定性：使用并发用未指定语义验证C程序
The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics
论文作者
论文摘要
我们提出了一种新颖且可自动化的方法，用于对C程序进行正式验证，以指定的语义验证，即一种流失某些评估的语言语义。首先，我们将此问题减少到并发系统的非确定性，从未指定的顺序C代码中自动提取分布式活动对象模型。这种翻译过程为经过的C子集提供了完全正式的语义。在提取的模型中，每个非确定性选择都对应于一个可能的评估顺序。此步骤还将自动将ANSI/ISO C规范语言（ACSL）中的规格转换为活动对象的方法合同和对象不变性。然后，我们使用Crowbar定理贵族对指定的活动对象模型进行验证，该模型验证了有关翻译规范的提取的模型，并确保C代码的原始属性为所有可能的评估订单。 通过使用模型提取，我们可以使用标准工具，而无需设计新的复杂程序逻辑来处理指定。所使用的案例研究被高度指定，无法通过现有工具正确处理。
We present a novel and well automatable approach to formal verification of C programs with underspecified semantics, i.e., a language semantics that leaves open the order of certain evaluations. First, we reduce this problem to non-determinism of concurrent systems, automatically extracting a distributed Active Object model from underspecified, sequential C code. This translation process provides a fully formal semantics for the considered C subset. In the extracted model every non-deterministic choice corresponds to one possible evaluation order. This step also automatically translates specifications in the ANSI/ISO C Specification Language (ACSL) into method contracts and object invariants for Active Objects. We then perform verification on the specified Active Objects model, using the Crowbar theorem prover, which verifies the extracted model with respect to the translated specification and ensures the original property of the C code for all possible evaluation orders. By using model extraction, we can use standard tools, without designing a new complex program logic to deal with underspecification. The case study used is highly underspecified and cannot be handled correctly by existing tools for C.
