We explore the oracle problem in automated repair of multi-fault programs, focusing on validating partial patches produced during incremental repair phases. Given a multi-fault program$P$with faults$f_{1}, \ldots, f_{n}$and a test suite$T$triggering these faults, the goal is to design validation oracles$\mathcal{O}^{(1)}, \ldots, \mathcal{O}^{(n)}$for intermediate patches$p t_{1}, \ldots, p t_{n}$that address individual faults. Validating partial patches raises two major issues. First, such patches are typically generated incrementally by APR tools and may address only a subset of the program's faults, leaving others unresolved. As a result, they often fail to produce correct outputs when evaluated in isolation. Second, validation must account for interactions with remaining faults to avoid rejecting valid fixes. To address these issues, we outline a validation framework that blends the strengths of output-based, halting, and assertion-based oracles, some of which are informed by bug reports. The framework provides a modular approach to assess both partial and composite patches in programs with multiple defects by integrating formal reasoning and modeling the interactions of faults. This conceptual framework lays the groundwork for more faultaware and interaction-sensitive repair techniques and moves us toward a deeper, more practical understanding of how to assess patch correctness in complex, real-world multi-fault scenarios.

Patch overfitting remains a persistent challenge in automated program repair (APR), especially when validation depends on incomplete test suites. We argue that this problem is significantly exacerbated by the overlooked presence of multiple interacting faults, a common yet under-addressed reality in real-world software. Conventional APR tools typically treat faults in isolation, neglecting subtle interactions that can mask faults or introduce regressions. To address this, we develop a taxonomy of five fault interaction-aware patch assessment strategies, supported by a formal model that identifies when and how each should be applied. Our framework guides robust multi-fault repair and exposes how fault interactions critically influence patch outcomes. To our knowledge, this is the first formal treatment of patch assessment and overfitting in multi-fault settings, offering a foundation for more reliable and practical APR.

Multi-fault programs, which contain more than one bug simultaneously, are notoriously difficult to debug and repair. This is largely because faults can interact in subtle ways: one might hide the effects of another, or even cause new failures to appear when combined. In this paper, we investigate why multi-fault programs remain so challenging for today’s debugging and repair tools. We introduce a formal model that captures the different ways faults can interact, including masking, synergy, and cascading. Building on this model, we propose a novel framework for reasoning about faults, not in isolation, but as part of a network of influences. This perspective opens the door for future tools that can better understand, diagnose, and repair programs with multiple faults.

Repairing a large-scale buggy program using current automated program repair (APR) approaches can be a difficult 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 (ORBS) 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. The paper concludes with a set of advice for successfully employing program reduction techniques in the context of APR.

Patch overfitting is a well-known open challenge for automated program repair (APR), which results from having insufficient or incomplete specifications to validate the generated patches. We argue that part of the patch overfitting challenge is caused by not properly taking termination issues into account during patch validation. As such, our goal here is to improve the APR process by proposing a new approach that is dedicated to more complete patch correctness validation for APR. The paper is divided into two parts: In the first part, we study the correlation between the automated program repair problem and the program termination problem, demonstrating how a variety of program defects (e.g., violation of liveness properties, which causes the program to run indefinitely, and memory safety properties, which lead the program to crash) can be handled by fixing the termination of the program. In the second part, we present a novel patch validation approach that extends the standard test-based validation strategy by verifying two additional oracles: (i) oracle Oeb, which is an assertion-based oracle, obtained from developer-written bug reports and used to check the absence of erroneous behavior associated with the analyzed bug, and (ii) oracle$\mathcal{O}_{halt}$, which is a halting oracle used to check the normal halting of the patched program. We demonstrate how to validate oracles$:\mathcal{O}_{eb}$and$\mathcal{O}_{halt}$using contemporary termination provers and program verifiers. We also demonstrate how to effectively use the new validation oracles while taking into account the type of bug being repaired and the structure of the defected program.

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}$$ φ correct and $$\varphi _{violated}$$ φ violated , where $$\varphi _{correct}$$ φ correct represents the set of likely invariants (good patterns) required for a run to be successful and $$\varphi _{violated}$$ φ 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.

Modern automated program repair (APR) tools are well-tuned at repairing single fault programs (i.e., programs in which only one fault can occur at time). However, real-world software projects typically contain multiple bugs at the same time, which can interact with and mask each other in a variety of ways. The complex interaction of faults in multi-fault programs makes the automated repair problem more challenging than the traditional practice of presuming that a program contains a single fault. This paper studies the repair problem of multi-fault programs and identifies the main obstacles that arise when handling such programs using current repair approaches. The paper also describes three repair approaches for multi-fault programs, namely iterative, parallel, and simultaneous. While the simultaneous repair strategy depends on using cutting-edge fault localization techniques that enable the APR approaches to locate many faults at once, the iterative and parallel repair approaches rely on adapting the existing repair techniques for single-fault programs to handle multi-fault programs. Finally, the paper discusses each approach's advantages and drawbacks as well as the conditions in which the approach can be used successfully. To our knowledge, this is the first paper to specifically study and address the repair problem of multi-fault programs.

This paper describes a formal repair framework for performance bugs in loop programs, which are programming errors that slow down program execution. The approach is developed based on the observation that a program with a performance bug is a semantically correct program, but it may perform inefficiently for some inputs. This observation permits the formal treatment of performance bugs using the idea of program invariants, where the original program is augmented with a number of non-functional variables that are used to assess the efficiency of the patched version vs. the original program using the derived invariants. The proposed approach offers two major advantages compared to the conventional test-based patch validation approach. First, it enables the formal validation of patches using program verifiers. Second, it helps to assess the efficiency boost provided by the generated patches. To the best of our knowledge, the formal treatment of performance bugs has not been studied in the prior literature.

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 observable behavior (e.g., termination bugs and non-functional bugs). Such bugs can generally not be handled with current APR approaches, so complementary techniques are needed. To stimulate the systematic study of alternative approaches and hybrid 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 study the repair of termination bugs in sequential and concurrent programs. Our analysis 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. We empirically investigate how well the hybrid approach can repair termination and performance bugs by experimenting with hybrids that integrate different APR approaches with termination provers and execution time monitors. Our findings indicate that hybrid repair holds promise for handling termination and performance bugs. However, the capability of the chosen tools and the completeness of the available correctness specification affects the quality of the patches that can be produced.

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.

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. A student-submitted program is aligned and composed with a reference solution in terms of control flow, and the variables of the two programs are automatically aligned via predicates describing the relationship between the variables. When verification attempt for the obtained aligned program fails, we turn a verification problem into a MaxSMT problem whose solution leads to a minimal repair. We have conducted experiments on student assignments curated from a widely deployed intelligent tutoring system. Our results show that generating verified repair without sacrificing the overall repair rate is possible. In fact, our implementation, Verifix, is shown to outperform Clara, a state-of-the-art tool, in terms of repair rate. This shows the promise of using verified repair to generate high confidence feedback in programming pedagogy settings.

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.

Smart contracts are automated or self-enforcing contracts that can be used to exchange assets without having to place trust in third parties. Many commercial transactions use smart contracts due to their potential benefits in terms of secure peer-to-peer transactions independent of external parties. Experience shows that many commonly used smart contracts are vulnerable to serious malicious attacks, which may enable attackers to steal valuable assets of involving parties. There is, therefore, a need to apply analysis and automated repair techniques to detect and repair bugs in smart contracts before being deployed. In this work, we present the first general-purpose automated smart contract repair approach that is also gas-aware. Our repair method is search-based and searches among mutations of the buggy contract. Our method also considers the gas usage of the candidate patches by leveraging our novel notion of gas dominance relationship . We have made our smart contract repair tool SCRepair available open-source, for investigation by the wider community.

This paper presents a novel framework for decentralized monitoring of Linear Temporal Logic (LTL) formulas, under the situation where processes are synchronous and the formula is represented as a tableau. The tableau technique allows one to construct a semantic tree for the input LTL formula, which can be used to optimize the decentralized monitoring of LTL in various ways. Given a system P and an LTL formula φ, we construct a tableau T φ . The tableau T φ is used for two purposes: (a) to synthesize an efficient round-robin communication policy for processes, and (b) to find the minimal ways to decompose the formula and communicate observations of processes in an efficient way. In our framework, processes can propagate truth values of both atomic and compound formulas (non-atomic formulas) depending on the syntactic structure of the input LTL formula and the observation power of processes. We demonstrate that this approach of decentralized monitoring based on tableau construction is more straightforward, more flexible, and more likely to yield efficient solutions than alternative approaches.

Abstract The paper presents a new efficient algorithm for computing worst case execution time (WCET) of systems modelled as timed automata (TA). The algorithm uses a set of abstraction techniques that improve significantly the efficiency of WCET analysis of TA models with cyclic behaviour. We show that the proposed abstractions are exact with respect to the WCET problem in the sense that the WCET computed in the abstract model is equal to the one computed in the concrete model. We also compare our algorithm with the one implemented in the model checker UPPAAL which shows that when infinite cycles exist (i.e. cycles that can be run infinitely often), UPPAAL’s algorithm may not terminate, and when largely repetitive finite cycles exist (i.e. cycles that can be run a large number of times but finite), UPPAAL’s algorithm suffers from the state space explosion, thus leading to a low efficiency or resource exhaustion.

We present a formal analysis of the well-known two phase atomic commitment protocol. The protocol is modeled as networks of timed automata using the model checker UPPAAL. The protocol has been verified in two different crash models, the crash-stop model, and the crash-recovery model. The paper also describes how dense-timed model checking technology may be applied to discover the worst case execution time and the corresponding worst-case scenario of the protocol. The analysis also allows us to illustrate various features of the UPPAAL tool, which shows that the specification language of the tool lacks the expressiveness to capture some desired properties of the protocol.

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. This result is applied to optimize model checking of implementations of a knowledge-based program 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.