-
On The Effectiveness of Dynamic Reduction Techniques in Automated Program Repair
Authors:
Omar I. Al-Bataineh
Abstract:
Repairing a large-scale buggy program using current automated program repair (APR) approaches can be a time-consuming operation that requires significant computational resources. We describe a program repair framework that effectively handles large-scale buggy programs of industrial complexity. The framework exploits program reduction in the form of program slicing to eliminate parts of the code i…
▽ More
Repairing a large-scale buggy program using current automated program repair (APR) approaches can be a time-consuming operation that requires significant computational resources. We describe a program repair framework that effectively handles large-scale buggy programs of industrial complexity. The framework exploits program reduction in the form of program slicing to eliminate parts of the code irrelevant to the bug being repaired without adversely affecting the capability of the repair system in producing correct patches.
Observation-based slicing is a recently introduced, language-independent slicing technique that shows a good effectiveness in a wide range of applications. In this work, we show how ORBS can be effectively integrated with APR to improve all aspects of the repair process including the fault localization step, patch generation step, and patch validation step. The presented repair framework indeed enhances the capability of APR by reducing the execution cost of a test suite and the search cost for the appropriate faulty statement corresponding to the bug being repair. Our empirical results on the widely used Defects4J dataset reveal that a substantial improvement in performance can be obtained without any degradation in repair quality.
△ Less
Submitted 23 June, 2024;
originally announced June 2024.
-
Invariant-based Program Repair
Authors:
Omar I. Al-Bataineh
Abstract:
This paper describes a formal general-purpose automated program repair (APR) framework based on the concept of program invariants. In the presented repair framework, the execution traces of a defected program are dynamically analyzed to infer specifications $\varphi_{correct}$ and $\varphi_{violated}$, where $\varphi_{correct}$ represents the set of likely invariants (good patterns) required for a…
▽ More
This paper describes a formal general-purpose automated program repair (APR) framework based on the concept of program invariants. In the presented repair framework, the execution traces of a defected program are dynamically analyzed to infer specifications $\varphi_{correct}$ and $\varphi_{violated}$, where $\varphi_{correct}$ represents the set of likely invariants (good patterns) required for a run to be successful and $\varphi_{violated}$ represents the set of likely suspicious invariants (bad patterns) that result in the bug in the defected program. These specifications are then refined using rigorous program analysis techniques, which are also used to drive the repair process towards feasible patches and assess the correctness of generated patches.We demonstrate the usefulness of leveraging invariants in APR by developing an invariant-based repair system for performance bugs. The initial analysis shows the effectiveness of invariant-based APR in handling performance bugs by producing patches that ensure program's efficiency increase without adversely impacting its functionality.
△ Less
Submitted 26 January, 2024; v1 submitted 27 December, 2023;
originally announced December 2023.
-
Towards Extending the Range of Bugs That Automated Program Repair Can Handle
Authors:
Omar I. Al-Bataineh,
Leon Moonen
Abstract:
Modern automated program repair (APR) is well-tuned to finding and repairing bugs that introduce observable erroneous behavior to a program. However, a significant class of bugs does not lead to such observable behavior (e.g., liveness/termination bugs, non-functional bugs, and information flow bugs). Such bugs can generally not be handled with current APR approaches, so, as a community, we need t…
▽ More
Modern automated program repair (APR) is well-tuned to finding and repairing bugs that introduce observable erroneous behavior to a program. However, a significant class of bugs does not lead to such observable behavior (e.g., liveness/termination bugs, non-functional bugs, and information flow bugs). Such bugs can generally not be handled with current APR approaches, so, as a community, we need to develop complementary techniques.
To stimulate the systematic study of alternative APR approaches and hybrid APR combinations, we devise a novel bug classification system that enables methodical analysis of their bug detection power and bug repair capabilities. To demonstrate the benefits, we analyze the repair of termination bugs in sequential and concurrent programs. The study shows that integrating dynamic APR with formal analysis techniques, such as termination provers and software model checkers, reduces complexity and improves the overall reliability of these repairs.
△ Less
Submitted 7 November, 2022;
originally announced November 2022.
-
Towards More Reliable Automated Program Repair by Integrating Static Analysis Techniques
Authors:
Omar I. Al-Bataineh,
Anastasiia Grishina,
Leon Moonen
Abstract:
A long-standing open challenge for automated program repair is the overfitting problem, which is caused by having insufficient or incomplete specifications to validate whether a generated patch is correct or not. Most available repair systems rely on weak specifications (i.e., specifications that are synthesized from test cases) which limits the quality of generated repairs. To strengthen specific…
▽ More
A long-standing open challenge for automated program repair is the overfitting problem, which is caused by having insufficient or incomplete specifications to validate whether a generated patch is correct or not. Most available repair systems rely on weak specifications (i.e., specifications that are synthesized from test cases) which limits the quality of generated repairs. To strengthen specifications and improve the quality of repairs, we propose to closer integrate static bug detection techniques with automated program repair. The integration combines automated program repair with static analysis techniques in such a way that bug detection patterns can be synthesized into specifications that the repair system can use. We explore the feasibility of such integration using two types of bugs: arithmetic bugs, such as integer overflow, and logical bugs, such as termination bugs. As part of our analysis, we make several observations that help to improve patch generation for these classes of bugs. Moreover, these observations assist with narrowing down the candidate patch search space, and inferring an effective search order.
△ Less
Submitted 10 November, 2021;
originally announced November 2021.
-
Verifix: Verified Repair of Programming Assignments
Authors:
Umair Z. Ahmed,
Zhiyu Fan,
Jooyong Yi,
Omar I. Al-Bataineh,
Abhik Roychoudhury
Abstract:
Automated feedback generation for introductory programming assignments is useful for programming education. Most works try to generate feedback to correct a student program by comparing its behavior with an instructor's reference program on selected tests. In this work, our aim is to generate verifiably correct program repairs as student feedback. The student assignment is aligned and composed wit…
▽ More
Automated feedback generation for introductory programming assignments is useful for programming education. Most works try to generate feedback to correct a student program by comparing its behavior with an instructor's reference program on selected tests. In this work, our aim is to generate verifiably correct program repairs as student feedback. The student assignment is aligned and composed with a reference solution in terms of control flow, and differences in data variables are automatically summarized via predicates to relate the variable names. Failed verification attempts for the equivalence of the two programs are exploited to obtain a collection of maxSMT queries, whose solutions point to repairs of the student assignment. We have conducted experiments on student assignments curated from a widely deployed intelligent tutoring system. Our results indicate that we can generate verified feedback in up to 58% of the assignments. More importantly, our system indicates when it is able to generate a verified feedback, which is then usable by novice students with high confidence.
△ Less
Submitted 30 June, 2021;
originally announced June 2021.
-
Verifying Real-time Commit Protocols Using Dense-time Model Checking Technology
Authors:
Omar I. Al-Bataineh,
Mark Reynolds
Abstract:
The timed-based automata model, introduced by Alur and Dill, provides a useful formalism for describing real-time systems. Over the last two decades, several dense-time model checking tools have been developed based on that model. The paper considers the verification of real-time distributed commit protocols using dense-time model checking technology. More precisely, we model and verify the well-k…
▽ More
The timed-based automata model, introduced by Alur and Dill, provides a useful formalism for describing real-time systems. Over the last two decades, several dense-time model checking tools have been developed based on that model. The paper considers the verification of real-time distributed commit protocols using dense-time model checking technology. More precisely, we model and verify the well-known timed two phase commit protocol in three different state-of-the-art real-time model checkers: UPPAAL, Rabbit, and RED, and compare the results.
△ Less
Submitted 10 May, 2018; v1 submitted 16 January, 2012;
originally announced January 2012.
-
Abstraction for Epistemic Model Checking of Dining Cryptographers-based Protocols
Authors:
Omar I. Al-Bataineh,
Ron van der Meyden
Abstract:
The paper describes an abstraction for protocols that are based on multiple rounds of Chaum's Dining Cryptographers protocol. It is proved that the abstraction preserves a rich class of specifications in the logic of knowledge, including specifications describing what an agent knows about other agents' knowledge. This result can be used to optimize model checking of Dining Cryptographers-based pro…
▽ More
The paper describes an abstraction for protocols that are based on multiple rounds of Chaum's Dining Cryptographers protocol. It is proved that the abstraction preserves a rich class of specifications in the logic of knowledge, including specifications describing what an agent knows about other agents' knowledge. This result can be used to optimize model checking of Dining Cryptographers-based protocols, and applied within a methodology for knowledge-based program implementation and verification. Some case studies of such an application are given, for a protocol that uses the Dining Cryptographers protocol as a primitive in an anonymous broadcast system. Performance results are given for model checking knowledge-based specifications in the concrete and abstract models of this protocol, and some new conclusions about the protocol are derived.
△ Less
Submitted 11 October, 2010;
originally announced October 2010.
-
Epistemic Model Checking for Knowledge-Based Program Implementation: an Application to Anonymous Broadcast
Authors:
Omar I. Al-Bataineh,
Ron van der Meyden
Abstract:
Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The paper describes how epistemic model checking technology may be applied to discover and verify concrete implementations based on this abstract level of description. The details of the implementations depend on the specific context of use of the protocol…
▽ More
Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The paper describes how epistemic model checking technology may be applied to discover and verify concrete implementations based on this abstract level of description. The details of the implementations depend on the specific context of use of the protocol. The knowledge-based approach enables the implementations to be optimized relative to these conditions of use. The approach is illustrated using extensions of the Dining Cryptographers protocol, a security protocol for anonymous broadcast.
△ Less
Submitted 25 April, 2010;
originally announced April 2010.
