Workshop APR 2026 – Author Index |
Contents -
Abstracts -
Authors
|
| Amaral, Isabel |
Isabel Amaral, Álvaro F. Silva, João F. Ferreira, and Alexandra Mendes (INESC TEC, Portugal; University of Porto, Portugal; INESC-ID, Portugal) Formal verification using verification-aware languages, like Dafny, ensures a program's conformance to its specification. Assuming a correct and complete specification, a verification failure may indicate an implementation fault that the developer must identify and correct. However, debugging verification failures is particularly challenging, as verification diagnostics do not directly hint at the implementation changes required for verification to succeed. Automated Program Repair has long been explored for traditional programming languages to reduce manual debugging effort, yet it remains largely underexplored in verification-aware contexts. We propose DafnyFix, a repair framework for Dafny that searches over a space of single-transformation candidate patches generated through three complementary heuristics: existing mutation testing operators, newly introduced repair-oriented mutation operators, and state-guided repair templates inspired by AutoFix. We evaluate DafnyFix’s effectiveness on a dataset of implementation faults in LLM-generated Dafny programs curated from the dafny-synthesis benchmark, and successfully repair 62.5% of the faults, showing that small deterministic transformations can repair a substantial number of faulty LLM-generated implementations. Our results further show that the proposed repair heuristics are complementary, targeting different categories of implementation faults. Additionally, we identify six fault patterns of LLM-generated programs in our dataset that can be corrected by small program transformations. |
|
| Bindschaedler, Laurent |
Bardia Mohammadi and Laurent Bindschaedler (MPI-SWS, Germany) Tests play two roles in automated program repair (APR): they are the evidence that accepts a patch, and they are repository artifacts that may themselves need repair. Benchmarks resolve the tension by making evaluator-owned tests immutable; deployment cannot, because tests legitimately evolve with the code they check. We argue that the resulting question, who may authorize a change to the evidence that accepts a patch, is a problem of allocating authority, distinct from whether a patch is correct, and that no diff separates an authorized change of requirements from an agent weakening its own acceptance test. We propose an admissible repair witness, evidence that exists before the agent runs and that the agent cannot rewrite, and a two-zone policy that protects it while the rest of the test surface evolves under review. In 230 merged bug-fix pull requests from nine repositories, 160 of 172 test-changing repairs (93.0%) edit a test artifact that already exists, so locking the test surface is not an option. Of the 172, 87 delete test lines, but only 53 delete an assertion, a test case, an expected output, or a whole test file: escalating on deleted lines alone sends half of all test-changing repairs to a human, while reading what was deleted sends at best under a third. |
|
| Cohen, Myra B. |
Md Al Muzahid Nayim, Faezeh Rajabi Kouchi, Amit Kumar Sikder, and Myra B. Cohen (Iowa State University, USA) Search-Based Software Testing relies on fitness functions to guide search algorithms toward target branches. Traditionally, computing fitness for branches involves a program analysis pipeline, with instrumentation that is language and type dependent. Large Language Models (LLMs) provide a promising mechanism for automatically generating branch aware executable fitness functions. However, directly using LLM generated outputs is unreliable, leading to incomplete outputs, compilation errors, or incorrect optimization objectives. This paper presents FitGen, a validation guided repair framework combining structured prompt design with output, syntax, and semantic validation to automatically diagnose and repair executable fitness functions. We evaluate FitGen on 11 benchmark programs containing 51 target branches using fitness functions generated by six state of the art LLMs. Our results show FitGen improves branch validation performance across all LLMs by up to 40.91% using the repaired fitness functions, and search based optimization achieves up to 93.59% branch validation accuracy. |
|
| Ferreira, João F. |
Isabel Amaral, Álvaro F. Silva, João F. Ferreira, and Alexandra Mendes (INESC TEC, Portugal; University of Porto, Portugal; INESC-ID, Portugal) Formal verification using verification-aware languages, like Dafny, ensures a program's conformance to its specification. Assuming a correct and complete specification, a verification failure may indicate an implementation fault that the developer must identify and correct. However, debugging verification failures is particularly challenging, as verification diagnostics do not directly hint at the implementation changes required for verification to succeed. Automated Program Repair has long been explored for traditional programming languages to reduce manual debugging effort, yet it remains largely underexplored in verification-aware contexts. We propose DafnyFix, a repair framework for Dafny that searches over a space of single-transformation candidate patches generated through three complementary heuristics: existing mutation testing operators, newly introduced repair-oriented mutation operators, and state-guided repair templates inspired by AutoFix. We evaluate DafnyFix’s effectiveness on a dataset of implementation faults in LLM-generated Dafny programs curated from the dafny-synthesis benchmark, and successfully repair 62.5% of the faults, showing that small deterministic transformations can repair a substantial number of faulty LLM-generated implementations. Our results further show that the proposed repair heuristics are complementary, targeting different categories of implementation faults. Additionally, we identify six fault patterns of LLM-generated programs in our dataset that can be corrected by small program transformations. |
|
| Guo, Taoer |
Taoer Guo (New York University, USA) Large Language Models (LLMs) are increasingly incorporated into verifier-in-the-loop software engineering systems, yet it remains unclear how the representation of verifier feedback affects their ability to repair incorrect programs. We study this question by isolating feedback representation from model, task, and prompting effects. We compare five feedback modalities ranging from binary verification status to natural language explanations, concrete counterexamples, and raw symbolic traces. We evaluate four open-weight code models spanning 7B to 480B total parameters on a 540-task benchmark combining controlled verification tasks with contractannotated problems derived from HumanEval+ and MBPP+. Counterexample feedback achieves the strongest repair performance across the evaluated models, while full symbolic traces provide substantially more information without yielding corresponding gains. A token-matched padding control shows that prompt length explains only part of the observed gap, while a redundant-feedback ablation shows that adding a full trace to an already actionable counterexample does not improve repair performance. These results suggest that the interface between formal verification and neural program repair should be treated as a representation problem rather than simply an information-maximization problem. |
|
| Jiang, Jiajun |
Jiajun Sun, Yaocai Zhao, Fengjie Li, and Jiajun Jiang (Tianjin University, China) Automated code translators can now produce repository-scale translations from Java to Python, yet a substantial fraction of translated functions remain semantically incorrect. Repairing such defects differs from traditional automated program repair (APR) because the correctness specification is based on the source language and no target-language test suite exists to guide fault localization. We observe that the original Java code is the most authoritative specification for repair and propose AnchorRepair, a dual-agent framework that treats the Java source as first-class diagnostic evidence. The Diagnosis Agent operates in a ReAct-style loop and autonomously invokes seven cross-lingual analysis tools, producing a structured root-cause diagnosis by contrasting the Java specification against the Python translation across control flow, data flow, and call graph dimensions. A Patch Agent then generates a corrected Python function conditioned on this diagnosis and the retrieved Java context. We evaluated AnchorRepair on 82 real translation defects from four Apache Commons projects. With DeepSeek-V3.2 as the backend, AnchorRepair repairs 40 defects (48.8%), a 12-point absolute improvement over the LLM-Only baseline (28/82) and substantially outperforming TransAgent (17/82) and D4C (21/82). The framework generalizes across LLM backends without modification and achieves repair coverage comparable to a general-purpose coding agent at less than half the cost. Our source code and all experimental results are publicly available at https://github.com/JJS-TJ/AnchorRepair. |
|
| Kado, Chihiro |
Chihiro Kado and Tatsuhiro Tsuchiya (University of Osaka, Japan) Smart contracts are at risk of significant financial losses due to vulnerabilities in their program logic. To mitigate such damages, various automated program repair tools have been proposed. However, existing tools, especially those based on Large Language Models (LLMs), may introduce unintended changes to the original functionality even when they successfully remove vulnerabilities. To improve the repair performance of LLM-based approaches while preserving functionality, we propose RAWL, a Retrieval-Augmented Generation (RAG)-based approach for smart contract vulnerability repair. RAWL incorporates a Weisfeiler-Lehman (WL) algorithm-based Abstract Syntax Tree (AST) retrieval mechanism as its RAG component. By applying the WL algorithm to ASTs, RAWL encodes the structural information of the vulnerability-related portion of the AST into a compact representation, enabling the retrieval of structurally relevant contracts as repair references. We evaluate RAWL and a non-RAG-based approach on 43 vulnerable contracts, executing each approach five times per contract, resulting in 215 generated outputs for both methods. RAWL produced 203 valid patches (93%) and at least one valid patch for all 43 contracts (100%), whereas the baseline approach produced 170 valid patches (79%) and at least one valid patch for 40 contracts (93%). The results indicate that RAWL effectively leveraged retrieved contracts when necessary, achieving higher repair performance than the non-RAG-based approach. |
|
| Kouchi, Faezeh Rajabi |
Md Al Muzahid Nayim, Faezeh Rajabi Kouchi, Amit Kumar Sikder, and Myra B. Cohen (Iowa State University, USA) Search-Based Software Testing relies on fitness functions to guide search algorithms toward target branches. Traditionally, computing fitness for branches involves a program analysis pipeline, with instrumentation that is language and type dependent. Large Language Models (LLMs) provide a promising mechanism for automatically generating branch aware executable fitness functions. However, directly using LLM generated outputs is unreliable, leading to incomplete outputs, compilation errors, or incorrect optimization objectives. This paper presents FitGen, a validation guided repair framework combining structured prompt design with output, syntax, and semantic validation to automatically diagnose and repair executable fitness functions. We evaluate FitGen on 11 benchmark programs containing 51 target branches using fitness functions generated by six state of the art LLMs. Our results show FitGen improves branch validation performance across all LLMs by up to 40.91% using the repaired fitness functions, and search based optimization achieves up to 93.59% branch validation accuracy. |
|
| Li, Fengjie |
Jiajun Sun, Yaocai Zhao, Fengjie Li, and Jiajun Jiang (Tianjin University, China) Automated code translators can now produce repository-scale translations from Java to Python, yet a substantial fraction of translated functions remain semantically incorrect. Repairing such defects differs from traditional automated program repair (APR) because the correctness specification is based on the source language and no target-language test suite exists to guide fault localization. We observe that the original Java code is the most authoritative specification for repair and propose AnchorRepair, a dual-agent framework that treats the Java source as first-class diagnostic evidence. The Diagnosis Agent operates in a ReAct-style loop and autonomously invokes seven cross-lingual analysis tools, producing a structured root-cause diagnosis by contrasting the Java specification against the Python translation across control flow, data flow, and call graph dimensions. A Patch Agent then generates a corrected Python function conditioned on this diagnosis and the retrieved Java context. We evaluated AnchorRepair on 82 real translation defects from four Apache Commons projects. With DeepSeek-V3.2 as the backend, AnchorRepair repairs 40 defects (48.8%), a 12-point absolute improvement over the LLM-Only baseline (28/82) and substantially outperforming TransAgent (17/82) and D4C (21/82). The framework generalizes across LLM backends without modification and achieves repair coverage comparable to a general-purpose coding agent at less than half the cost. Our source code and all experimental results are publicly available at https://github.com/JJS-TJ/AnchorRepair. |
|
| Mendes, Alexandra |
Isabel Amaral, Álvaro F. Silva, João F. Ferreira, and Alexandra Mendes (INESC TEC, Portugal; University of Porto, Portugal; INESC-ID, Portugal) Formal verification using verification-aware languages, like Dafny, ensures a program's conformance to its specification. Assuming a correct and complete specification, a verification failure may indicate an implementation fault that the developer must identify and correct. However, debugging verification failures is particularly challenging, as verification diagnostics do not directly hint at the implementation changes required for verification to succeed. Automated Program Repair has long been explored for traditional programming languages to reduce manual debugging effort, yet it remains largely underexplored in verification-aware contexts. We propose DafnyFix, a repair framework for Dafny that searches over a space of single-transformation candidate patches generated through three complementary heuristics: existing mutation testing operators, newly introduced repair-oriented mutation operators, and state-guided repair templates inspired by AutoFix. We evaluate DafnyFix’s effectiveness on a dataset of implementation faults in LLM-generated Dafny programs curated from the dafny-synthesis benchmark, and successfully repair 62.5% of the faults, showing that small deterministic transformations can repair a substantial number of faulty LLM-generated implementations. Our results further show that the proposed repair heuristics are complementary, targeting different categories of implementation faults. Additionally, we identify six fault patterns of LLM-generated programs in our dataset that can be corrected by small program transformations. |
|
| Mohammadi, Bardia |
Bardia Mohammadi and Laurent Bindschaedler (MPI-SWS, Germany) Tests play two roles in automated program repair (APR): they are the evidence that accepts a patch, and they are repository artifacts that may themselves need repair. Benchmarks resolve the tension by making evaluator-owned tests immutable; deployment cannot, because tests legitimately evolve with the code they check. We argue that the resulting question, who may authorize a change to the evidence that accepts a patch, is a problem of allocating authority, distinct from whether a patch is correct, and that no diff separates an authorized change of requirements from an agent weakening its own acceptance test. We propose an admissible repair witness, evidence that exists before the agent runs and that the agent cannot rewrite, and a two-zone policy that protects it while the rest of the test surface evolves under review. In 230 merged bug-fix pull requests from nine repositories, 160 of 172 test-changing repairs (93.0%) edit a test artifact that already exists, so locking the test surface is not an option. Of the 172, 87 delete test lines, but only 53 delete an assertion, a test case, an expected output, or a whole test file: escalating on deleted lines alone sends half of all test-changing repairs to a human, while reading what was deleted sends at best under a third. |
|
| Nayim, Md Al Muzahid |
Md Al Muzahid Nayim, Faezeh Rajabi Kouchi, Amit Kumar Sikder, and Myra B. Cohen (Iowa State University, USA) Search-Based Software Testing relies on fitness functions to guide search algorithms toward target branches. Traditionally, computing fitness for branches involves a program analysis pipeline, with instrumentation that is language and type dependent. Large Language Models (LLMs) provide a promising mechanism for automatically generating branch aware executable fitness functions. However, directly using LLM generated outputs is unreliable, leading to incomplete outputs, compilation errors, or incorrect optimization objectives. This paper presents FitGen, a validation guided repair framework combining structured prompt design with output, syntax, and semantic validation to automatically diagnose and repair executable fitness functions. We evaluate FitGen on 11 benchmark programs containing 51 target branches using fitness functions generated by six state of the art LLMs. Our results show FitGen improves branch validation performance across all LLMs by up to 40.91% using the repaired fitness functions, and search based optimization achieves up to 93.59% branch validation accuracy. |
|
| Reiss, Steven P. |
Steven P. Reiss (Brown University, USA) We argue that the use of test cases and extensive test suites to drive APR is harmful to the field and we push for something better. Such test suites are rare in practice. Moreover, using test cases for APR tends to skew how and where APR is used and bias experiments that attempt to validate its techniques. We suggest that other approaches to APR which do not assume such test suites are available are more appropriate. We also suggest developing new means for evaluating APR systems that do not depend solely on test-case-based examples. We challenge researchers to create such approaches and evaluations for a broad range of problems |
|
| Sikder, Amit Kumar |
Md Al Muzahid Nayim, Faezeh Rajabi Kouchi, Amit Kumar Sikder, and Myra B. Cohen (Iowa State University, USA) Search-Based Software Testing relies on fitness functions to guide search algorithms toward target branches. Traditionally, computing fitness for branches involves a program analysis pipeline, with instrumentation that is language and type dependent. Large Language Models (LLMs) provide a promising mechanism for automatically generating branch aware executable fitness functions. However, directly using LLM generated outputs is unreliable, leading to incomplete outputs, compilation errors, or incorrect optimization objectives. This paper presents FitGen, a validation guided repair framework combining structured prompt design with output, syntax, and semantic validation to automatically diagnose and repair executable fitness functions. We evaluate FitGen on 11 benchmark programs containing 51 target branches using fitness functions generated by six state of the art LLMs. Our results show FitGen improves branch validation performance across all LLMs by up to 40.91% using the repaired fitness functions, and search based optimization achieves up to 93.59% branch validation accuracy. |
|
| Silva, Álvaro F. |
Isabel Amaral, Álvaro F. Silva, João F. Ferreira, and Alexandra Mendes (INESC TEC, Portugal; University of Porto, Portugal; INESC-ID, Portugal) Formal verification using verification-aware languages, like Dafny, ensures a program's conformance to its specification. Assuming a correct and complete specification, a verification failure may indicate an implementation fault that the developer must identify and correct. However, debugging verification failures is particularly challenging, as verification diagnostics do not directly hint at the implementation changes required for verification to succeed. Automated Program Repair has long been explored for traditional programming languages to reduce manual debugging effort, yet it remains largely underexplored in verification-aware contexts. We propose DafnyFix, a repair framework for Dafny that searches over a space of single-transformation candidate patches generated through three complementary heuristics: existing mutation testing operators, newly introduced repair-oriented mutation operators, and state-guided repair templates inspired by AutoFix. We evaluate DafnyFix’s effectiveness on a dataset of implementation faults in LLM-generated Dafny programs curated from the dafny-synthesis benchmark, and successfully repair 62.5% of the faults, showing that small deterministic transformations can repair a substantial number of faulty LLM-generated implementations. Our results further show that the proposed repair heuristics are complementary, targeting different categories of implementation faults. Additionally, we identify six fault patterns of LLM-generated programs in our dataset that can be corrected by small program transformations. |
|
| Smytzek, Marius |
Marius Smytzek (CISPA Helmholtz Center for Information Security, Germany) Automated program repair (APR) has progressed in fault localization, patch generation, and validation, yet most still operate on a failure’s symptoms: failing tests, stack traces, and coverage. Fault localization derives a weak, positional explanation of where a fault may reside, but little about why it occurs. In contrast, developers build a richer account connecting the failure to its cause. That refinement is largely absent from APR, a gap between debugging and repair. We introduce failure explanations as a first-class APR artifact, recasting fault localization, statistical and semantic debugging, execution features, and causal reasoning as progressively richer explanations. Building on this perspective, we propose explanation-centric APR refining localization into a behavioral, causal explanation before repair, outlining the challenges of representing, generating, evaluating, and exploiting it. Marius Smytzek (CISPA Helmholtz Center for Information Security, Germany) Statistical fault localization traditionally correlates the execution of individual lines with test outcomes. A recent study of execution features argued that program behavior is far richer than line coverage. On 310 Python bugs, features such as scalar pairs, def-use pairs, and variable values correlated with failures and supported fault localization, while feature combinations reduced debugging effort beyond any single feature. Their generality across languages remains an open question. We replicate that study on Java. Using jSFLKit, an execution-feature recorder we built for Java, we collect the same 17 execution features across 516 bugs from 13 Defects4J projects, repeat the original correlation, localization, and multi-feature analyses, and compare the two languages. The original study’s main conclusions transfer to Java. Value- and data-level features correlate more strongly with failures than plain coverage, lines remain the strongest single feature for exact localization, and combining features improves the EXAM score, the share of a program a developer examines before reaching the fault. Our replication assesses the external validity of execution-feature debugging across programming languages and ecosystem compatibility, and contributes the first execution-feature fault-localization dataset for Java. |
|
| Sun, Jiajun |
Jiajun Sun, Yaocai Zhao, Fengjie Li, and Jiajun Jiang (Tianjin University, China) Automated code translators can now produce repository-scale translations from Java to Python, yet a substantial fraction of translated functions remain semantically incorrect. Repairing such defects differs from traditional automated program repair (APR) because the correctness specification is based on the source language and no target-language test suite exists to guide fault localization. We observe that the original Java code is the most authoritative specification for repair and propose AnchorRepair, a dual-agent framework that treats the Java source as first-class diagnostic evidence. The Diagnosis Agent operates in a ReAct-style loop and autonomously invokes seven cross-lingual analysis tools, producing a structured root-cause diagnosis by contrasting the Java specification against the Python translation across control flow, data flow, and call graph dimensions. A Patch Agent then generates a corrected Python function conditioned on this diagnosis and the retrieved Java context. We evaluated AnchorRepair on 82 real translation defects from four Apache Commons projects. With DeepSeek-V3.2 as the backend, AnchorRepair repairs 40 defects (48.8%), a 12-point absolute improvement over the LLM-Only baseline (28/82) and substantially outperforming TransAgent (17/82) and D4C (21/82). The framework generalizes across LLM backends without modification and achieves repair coverage comparable to a general-purpose coding agent at less than half the cost. Our source code and all experimental results are publicly available at https://github.com/JJS-TJ/AnchorRepair. |
|
| Tsuchiya, Tatsuhiro |
Chihiro Kado and Tatsuhiro Tsuchiya (University of Osaka, Japan) Smart contracts are at risk of significant financial losses due to vulnerabilities in their program logic. To mitigate such damages, various automated program repair tools have been proposed. However, existing tools, especially those based on Large Language Models (LLMs), may introduce unintended changes to the original functionality even when they successfully remove vulnerabilities. To improve the repair performance of LLM-based approaches while preserving functionality, we propose RAWL, a Retrieval-Augmented Generation (RAG)-based approach for smart contract vulnerability repair. RAWL incorporates a Weisfeiler-Lehman (WL) algorithm-based Abstract Syntax Tree (AST) retrieval mechanism as its RAG component. By applying the WL algorithm to ASTs, RAWL encodes the structural information of the vulnerability-related portion of the AST into a compact representation, enabling the retrieval of structurally relevant contracts as repair references. We evaluate RAWL and a non-RAG-based approach on 43 vulnerable contracts, executing each approach five times per contract, resulting in 215 generated outputs for both methods. RAWL produced 203 valid patches (93%) and at least one valid patch for all 43 contracts (100%), whereas the baseline approach produced 170 valid patches (79%) and at least one valid patch for 40 contracts (93%). The results indicate that RAWL effectively leveraged retrieved contracts when necessary, achieving higher repair performance than the non-RAG-based approach. |
|
| Zhao, Yaocai |
Jiajun Sun, Yaocai Zhao, Fengjie Li, and Jiajun Jiang (Tianjin University, China) Automated code translators can now produce repository-scale translations from Java to Python, yet a substantial fraction of translated functions remain semantically incorrect. Repairing such defects differs from traditional automated program repair (APR) because the correctness specification is based on the source language and no target-language test suite exists to guide fault localization. We observe that the original Java code is the most authoritative specification for repair and propose AnchorRepair, a dual-agent framework that treats the Java source as first-class diagnostic evidence. The Diagnosis Agent operates in a ReAct-style loop and autonomously invokes seven cross-lingual analysis tools, producing a structured root-cause diagnosis by contrasting the Java specification against the Python translation across control flow, data flow, and call graph dimensions. A Patch Agent then generates a corrected Python function conditioned on this diagnosis and the retrieved Java context. We evaluated AnchorRepair on 82 real translation defects from four Apache Commons projects. With DeepSeek-V3.2 as the backend, AnchorRepair repairs 40 defects (48.8%), a 12-point absolute improvement over the LLM-Only baseline (28/82) and substantially outperforming TransAgent (17/82) and D4C (21/82). The framework generalizes across LLM backends without modification and achieves repair coverage comparable to a general-purpose coding agent at less than half the cost. Our source code and all experimental results are publicly available at https://github.com/JJS-TJ/AnchorRepair. |
20 authors
proc time: 0.81