ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications
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.
At a high level, ICEBAR is an iterative, counterexample-based process, that generates and validates repair candidates. ICEBAR receives a faulty Alloy specification with a failing property-based oracle, and uses Alloy’s counterexamples to build tests and feed ARepair, a test-based Alloy repair tool, in order to produce a repair candidate. The candidate is then checked against the property oracle for overfitting: if the candidate passes, a repair has been found; if not, further counterexamples are generated to construct tests and enhance the test suite, and the process is iterated. ICEBAR includes different mechanisms, with different degrees of reliability, to generate counterexamples from failing predicates and assertions.
Our evaluation shows that ICEBAR significantly improves over ARepair, in both reducing overfitting and improving the repair rate. Moreover, ICEBAR shows that iterative refinement allows us to significantly improve a state-of-the-art tool for automated repair of Alloy specifications without any modifications to the tool.
Thu 13 OctDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 15:30
|ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications|
Simón Gutiérrez Brida University of Rio Cuarto and CONICET, Argentina, Germán Regis Universidad Nacional de Río Cuarto, Guolong Zheng University of Nebraska Lincoln, Hamid Bagheri University of Nebraska-Lincoln, ThanhVu Nguyen George Mason University, Nazareno Aguirre University of Rio Cuarto and CONICET, Argentina, Marcelo F. Frias Dept. of Software Engineering Instituto Tecnológico de Buenos Aires
|Repairing Failure-inducing Inputs with Input Reflection|
|ElecDaug: Electromagnetic Data Augmentation for Model Repair based on Metamorphic Relation|
|TransplantFix: Graph Differencing-based Code Transplantation for Automated Program RepairVirtual|
Deheng Yang National University of Defense Technology, Xiaoguang Mao National University of Defense Technology, Liqian Chen National University of Defense Technology, China, Xuezheng Xu Academy of Military Sciences, Beijing, China, Yan Lei Chongqing University, David Lo Singapore Management University, Jiayu He National University of Defense Technology, Changsha, China
Vision and Emerging Results
|Multi-objective Optimization-based Bug-fixing Template Mining for Automated Program RepairVirtual|
|StandUp4NPR: Standardizing Setup for Empirically Comparing Neural Program Repair SystemsVirtual|
Wenkang Zhong State Key Laboratory for Novel Software and Technology, Nanjing University, 22 Hankou Road, Nanjing, China, Hongliang Ge State Key Laboratory for Novel Software and Technology, Nanjing University, 22 Hankou Road, Nanjing, China, Hongfei Ai State Key Laboratory for Novel Software and Technology, Nanjing University, 22 Hankou Road, Nanjing, China, Chuanyi Li State Key Laboratory for Novel Software Technology, Nanjing University, Kui Liu Huawei Software Engineering Application Technology Lab, Jidong Ge , Bin Luo Software Institute, Nanjing University