程序模下的归纳谓词合成（扩展版）
软件工程
2024-07-12 v1
摘要
程序分析中的一个趋势是将验证条件编码在输入程序的语言中。这一做法通过利用即插即用的验证器简化了分析工具的设计，但使得与底层求解器的通信变得更加具有挑战性。本质上，分析器 operates at the level of input programs，而求解器 operates at the level of problem encodings。为桥接这一差距，验证器必须将分析器传递给求解器的证明规则。例如，基于归纳程序验证器构建的并发程序分析器可能需要为底层求解器声明 Owicki-Gries 风格的证明规则。每一种这样的证明规则都进一步指定了如何验证该程序，意味着传递证明规则的问题实际上是一种不变式合成的形式。类似地，许多程序分析任务归约为相对于程序合成纯、无循环的布尔函数（即谓词）。基于此，我们提出归纳谓词合成模程序 (IPS-MP)，该方法在输入语言中引入最小的合成功能以引导分析。在 IPS-MP 中，未知谓词出现在 assume 和 assert 语句中，作为程序语义的规约说明。现有的合成求解器在 IPS-MP 上效率不高，因为它们针对的是更通用问题。本文表明，IPS-MP 在布尔情况下的解是高效的，尽管其通常是不可判定的。此外，我们表明 IPS-MP 归约为受约束 Horn 子句的满足性，这比现有的合成问题更一般，却足以编码验证任务。我们提供了从具有挑战性验证任务（如参数化模型检查）到 IPS-MP 的归约。我们基于 SeaHorn 实现了这些归约的高效 IPS-MP 求解器，并描述了一个用于智能合约验证的应用。
引用
@article{arxiv.2407.08455,
title = {Inductive Predicate Synthesis Modulo Programs (Extended)},
author = {Scott Wesley and Maria Christakis and Jorge A. Navas and Richard Trefler and Valentin Wüstholz and Arie Gurfinkel},
journal= {arXiv preprint arXiv:2407.08455},
year = {2024}
}