论文标题
假设，保证或维修 - 非常规属性的常规框架（完整版）
Assume, Guarantee or Repair -- A Regular Framework for Non Regular Properties (full version)
论文作者
论文摘要
我们提出了假设 - 保证修复（AGR） - 一个新颖的框架，该框架验证程序是否满足一组属性，并在验证失败的情况下修复程序。我们考虑交流程序 - 这些是简单的类似C的程序，并通过交流渠道进行了同步操作扩展。我们的方法包括一种基于学习的方法来承担保证推理，同时执行验证和维修：在每种迭代中，AGR要么迈向证明（当前）系统满足所需属性，要么以使其更接近满足这些属性的方式来改变系统。为了处理无限状态系统，我们构建有限的抽象，为此我们使用句法和语义感知方法来检查包含一阶约束的复杂属性的满意度。我们实施了AGR，并根据各种通信协议进行了评估。我们的实验提出了紧凑的正确性证明和快速维修。
We present Assume-Guarantee-Repair (AGR) - a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs - these are simple C-like programs, extended with synchronous actions over communication channels. Our method, which consists of a learning-based approach to assume-guarantee reasoning, performs verification and repair simultaneously: in every iteration, AGR either makes another step towards proving that the (current) system satisfies the required properties, or alters the system in a way that brings it closer to satisfying the properties. To handle infinite-state systems we build finite abstractions, for which we check the satisfaction of complex properties that contain first-order constraints, using both syntactic and semantic-aware methods. We implemented AGR and evaluated it on various communication protocols. Our experiments present compact proofs of correctness and quick repairs.
