ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications
Abstract
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.
BibTeX
@inproceedings{Brida-al:ASE22,
author = {Sim{\'{o}}n Guti{\'{e}}rrez Brida and
Germ{\'{a}}n Regis and
Guolong Zheng and
Hamid Bagheri and
ThanhVu Nguyen and
Nazareno Aguirre and
Marcelo F. Frias},
title = {{ICEBAR:} {Feedback-Driven} Iterative Repair of Alloy Specifications},
booktitle = {ASE},
pages = {55:1--55:13},
publisher = {{ACM}},
year = {2022},
}