合适的非确定性：利用并发性验证具有未指定语义的C程序
摘要：一种新的、可自动化的方法：形式化验证C程序的不完全规范语义，即，一种语义上还未确定特定评估顺序的语言。首先，将这个问题简化为并发系统的非确定性，并自动从不完全规范的顺序C代码中提取出一个分布式活动对象模型。这个转换过程为所考虑的C子集提供完全形式化的语义。在提取的模型中，每个非确定性选择对应一种可能的评估顺序。此步骤还会自动将ANSI/ISO C规范语言（ACSL）中的规范转换为活动对象的方法契约和对象不变式。然后，使用Crowbar定理证明器对指定的活动对象模型进行验证，验证提取的模型是否符合翻译后的规范，并确保C代码在所有可能的评估顺序下仍满足原始属性。通过使用模型提取，我们可以使用标准工具，而无需设计新的复杂程序逻辑来处理不完全规范。使用的案例研究高度不完全规范，现有的C工具无法正确处理。
作者：Eduard Kamburjan (University of Oslo, Oslo, Norway), Nathan Wasser (Sharpmind, Frankfurt, Germany)
论文ID：2208.04630
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-08-10