一句话：提出 ICEBAR，以 Alloy 规约中固有的断言与谓词作为性质型 oracle，迭代修复规约并缓解过拟合。
自动程序修复（APR）在 C、Java 等语言上已取得显著成效，但将其用于形式规约修复的研究仍较少。本文面向 Alloy 规约语言提出 ICEBAR：与多数依赖测试用例作为判定 oracle 的 APR 工具不同，ICEBAR 使用 Alloy 规约中天然存在的性质型 oracle——谓词与断言——来评估候选补丁，并以反馈驱动的迭代方式逐步修复规约。作者指出，性质型 oracle 的判定条件强于测试用例，可缓解 APR 中常见的过拟合问题；同时，断言与谓词是 Alloy 规约的固有部分而测试用例并非如此，因此该工具比基于测试的规约修复工具更贴近 Alloy 用户的使用方式。摘要未报告具体实验数据与基准。
Automated program repair (APR) techniques have shown great success in automatically finding fixes for programs in programming languages such as C or Java. In this work, we focus on repairing formal specifications, in particular for the Alloy specification language. As opposed to most APR tools, our approach to repair Alloy specifications, named ICEBAR, does not use test-based oracles for patch assessment. Instead, ICEBAR relies on the use of property-based oracles, commonly found in Alloy specifications as predicates and assertions. These property-based oracles define stronger conditions for patch assessment, thus reducing the notorious overfitting issue caused by using test-based oracles, typically observed in APR contexts. Moreover, as assertions and predicates are inherent to Alloy, whereas test cases are not, our tool is potentially more appealing to Alloy users than test-based Alloy repair tools.
@inproceedings{paperbot7192,
title = {ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications},
author = {Simón Gutiérrez Brida and Germán Regis and Guolong Zheng and Hamid Bagheri and Thanhvu Nguyen and Nazareno Aguirre and Marcelo Frias},
booktitle = {ASE},
year = {2022},
doi = {10.1145/3551349.3556944}
}