paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Automated model repair for Alloy

Alloy 模型的自动修复
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 3/10 · 该论文研究 Alloy 模型的自动修复,结合变异测试与程序合成,属于传统程序修复与形式化方法领域,但未涉及用户核心关注的 LLM/Agent 与静态分析/形式化验证的交叉,也未涉及浮点或贝叶斯程序分析。引用 42 inbox
Kaiyuan Wang, Allison Sullivan, Sarfraz Khurshid
crossref: 2026-09-12

AI 速览

一句话:提出首个 Alloy 模型自动修复技术 ARepair,融合变异测试与程序合成,修复 28/38 个真实缺陷模型。

自动程序修复已有大量研究,但主要面向 Java 等命令式代码,未覆盖 Alloy 这类带传递闭包的一阶关系逻辑声明式模型。本文提出首个 Alloy 模型修复技术 ARepair:以含失败用例的测试集为规约,先利用变异测试定位与生成候选修复成分,再借助程序合成搜索满足测试的模型修改,输出对给定测试正确的修复后模型。作者在收集的 38 个真实缺陷 Alloy 模型上进行评估,共成功修复 28 个,表明将自动修复、变异测试与合成相结合可有效修复声明式模型。

问题
现有自动程序修复主要针对命令式代码,如何修复 Alloy 声明式模型尚缺研究。
方法
ARepair 以含失败测试的测试集为输入,结合变异测试与程序合成,搜索并输出通过测试的修复模型。
评估
在收集的 38 个真实 Alloy 缺陷模型上评估,成功修复其中 28 个。
原文摘要(Abstract)

Automated program repair is an active research area. However, existing research focuses mostly on imperative code, e.g. in Java. In this paper, we study the problem of repairing declarative models in Alloy -- a first order relational logic with transitive closure. We introduce ARepair, the first technique for repairing Alloy models. ARepair follows the spirit of traditional automated program repair techniques. Specifically, ARepair takes as input a faulty Alloy model and a test suite that contains some failing test, and outputs a repaired model that is correct with respect to the given tests. ARepair integrates ideas from mutation testing and program synthesis to provide an effective solution for repairing Alloy models. The experimental results show that ARepair can fix 28 out of 38 real-world faulty models we collected.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot4730,
  title = {Automated model repair for Alloy},
  author = {Kaiyuan Wang and Allison Sullivan and Sarfraz Khurshid},
  booktitle = {ASE},
  year = {2018},
  doi = {10.1145/3238147.3238162}
}