假设、保证或修复——非规则属性的常规框架（完整版）
摘要：假设-保证-修复（AGR）：一种新颖的框架，用于验证程序是否满足一组属性，并在验证失败的情况下修复程序。我们考虑通信程序-这些是简单的C样式程序，通过通信通道扩展了同步操作。我们的方法包括基于学习的假设保证推理，同时进行验证和修复：在每次迭代中，AGR要么朝向证明当前系统满足所需属性迈出一步，要么改变系统的方式使其更接近满足属性。为了处理无限状态系统，我们构建了有限的抽象，对其中包含一阶约束的复杂属性进行满足性检查，使用了语法和语义感知的方法。我们实现了AGR并在各种通信协议上进行了评估。我们的实验提供了紧凑的正确性证明和快速修复。
作者：Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu and Sarai Sheinvald
论文ID：2207.10534
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-07-22