A formal definition of loop unrolling with applications to test coverage
- URL: http://arxiv.org/abs/2403.08923v2
- Date: Mon, 12 Aug 2024 17:31:01 GMT
- Title: A formal definition of loop unrolling with applications to test coverage
- Authors: Bertrand Meyer,
- Abstract summary: Techniques to achieve various forms of test coverage, such as branch coverage, typically do not iterate loops.
More recent work has shown that by "unrolling" loops the approach can find significantly more bugs.
- Score: 37.48416208168878
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Techniques to achieve various forms of test coverage, such as branch coverage, typically do not iterate loops; in other words, they treat a loop as a conditional, executed zero or one time. Existing work by the author and collaborators produces test suites guaranteeing full branch coverage. More recent work has shown that by "unrolling" loops the approach can find significantly more bugs. The present discussion provides the theoretical basis and precise definition for this concept of unrolling. While initially motivated by the need to improve standard test coverage practices (which execute loop bodies only once), to better testing coverage, the framework presented here is applicable to any form of reasoning about loops.
Related papers
- Efficient Dynamic Test Case Generation for Path-Based Coverage Criteria [2.099922236065961]
We present a novel approach to test-case generation that satisfies four white-box, path-based coverage criteria.<n>Our method builds on a modified version of Johnson algorithm and enables test cases to be generated incrementally and on demand.
arXiv Detail & Related papers (2026-02-21T09:26:23Z) - Reasoning about concurrent loops and recursion with rely-guarantee rules [0.0]
We present general, mechanically verified, refinement for reasoning about programs and loops.<n>We make use of the lattice-guarantee approach to that facilitates reasoning about interference from concurrent threads.
arXiv Detail & Related papers (2025-12-06T01:57:42Z) - Formalizing Regression Testing for Agile and Continuous Integration Environments [0.0]
We formalize the phenomenon of continuous or near-continuous regression testing using successive builds as a time-ordered chain.<n>We also formalize the regression test window between any two builds, which captures the limited time budget available for regression testing.
arXiv Detail & Related papers (2025-11-04T18:31:06Z) - Studying the Impact of Early Test Termination Due to Assertion Failure on Code Coverage and Spectrum-based Fault Localization [48.22524837906857]
This study is the first empirical study on early test termination due to assertion failure.
We investigated 207 versions of 6 open-source projects.
Our findings indicate that early test termination harms both code coverage and the effectiveness of spectrum-based fault localization.
arXiv Detail & Related papers (2025-04-06T17:14:09Z) - Loop unrolling: formal definition and application to testing [33.432652829284244]
Testing processes usually aim at high coverage, but loops severely limit coverage ambitions since the number of iterations is generally not predictable.
This article provides a formal definition and a set of formal properties of unrolling.
Using this definition as the conceptual basis, we have applied an unrolling strategy to an existing automated testing framework.
arXiv Detail & Related papers (2025-02-21T15:36:21Z) - CLOVER: A Test Case Generation Benchmark with Coverage, Long-Context, and Verification [71.34070740261072]
This paper presents a benchmark, CLOVER, to evaluate models' capabilities in generating and completing test cases.
The benchmark is containerized for code execution across tasks, and we will release the code, data, and construction methodologies.
arXiv Detail & Related papers (2025-02-12T21:42:56Z) - DOCE: Finding the Sweet Spot for Execution-Based Code Generation [69.5305729627198]
We propose a comprehensive framework that includes candidate generation, $n$-best reranking, minimum Bayes risk (MBR) decoding, and self-ging as the core components.
Our findings highlight the importance of execution-based methods and the difference gap between execution-based and execution-free methods.
arXiv Detail & Related papers (2024-08-25T07:10:36Z) - Benchmarking Video Frame Interpolation [11.918489436283748]
We present a benchmark which establishes consistent error metrics by utilizing a submission website that computes them.
We also present a test set adhering to the assumption of linearity by utilizing synthetic data, and evaluate the computational efficiency in a coherent manner.
arXiv Detail & Related papers (2024-03-25T19:13:12Z) - Self-Infilling Code Generation [60.12883980846781]
We introduce self-infilling code generation, a general framework that incorporates infilling operations into auto-regressive decoding.
We utilize this capability to introduce novel interruption and looping mechanisms in conventional decoding.
Our proposed decoding process is effective in enhancing both regularity and quality across several code generation benchmarks.
arXiv Detail & Related papers (2023-11-29T16:02:06Z) - Understanding prompt engineering may not require rethinking
generalization [56.38207873589642]
We show that the discrete nature of prompts, combined with a PAC-Bayes prior given by a language model, results in generalization bounds that are remarkably tight by the standards of the literature.
This work provides a possible justification for the widespread practice of prompt engineering.
arXiv Detail & Related papers (2023-10-06T00:52:48Z) - Program Structure Aware Precondition Generation [8.797622429151861]
We introduce a novel approach for inferring natural preconditions from code.
Our innovation lies in leveraging the structure of a target method as a seed to infer a precondition through program transformations.
We present a dataset of 18k Java (method, precondition) pairs obtained by applying our framework to 87 real-world projects.
arXiv Detail & Related papers (2023-10-03T15:40:19Z) - Seeding Contradiction: a fast method for generating full-coverage test
suites [36.52277143058971]
A test suite is a key resource for managing program evolution.
Seeding Contradiction inserts incorrect instructions into every basic block of the program.
The method is static, works fast, and achieves excellent coverage.
arXiv Detail & Related papers (2023-09-08T09:37:11Z) - Semi-Oblivious Chase Termination for Linear Existential Rules: An
Experimental Study [5.936402320555635]
The chase procedure is a fundamental algorithmic tool in databases that allows us to reason with constraints.
It takes as input a database and a set of constraints, and iteratively completes the database as dictated by the constraints.
A key challenge, though, is the fact that it may not terminate, which leads to the problem of checking whether it terminates given a database and a set of constraints.
arXiv Detail & Related papers (2023-03-22T18:21:01Z) - MPE inference using an Incremental Build-Infer-Approximate Paradigm [0.0]
Exact inference of the most probable explanation (MPE) in Bayesian networks is known to be NP-complete.
We propose an algorithm for approximate MPE inference that is based on the incremental build-infer-approximate framework.
The accuracy of our solution is comparable to a branch and bound search in majority of the benchmarks, with competitive run times.
arXiv Detail & Related papers (2022-06-04T09:37:44Z) - A Call for Clarity in Beam Search: How It Works and When It Stops [125.55175954381991]
We introduce a patience factor, a simple modification to this beam decoding implementation, that generalizes the stopping criterion and provides flexibility to the depth of search.
Empirical results demonstrate that adjusting this patience factor improves decoding performance of strong pretrained models on news text summarization and machine translation over diverse language pairs.
arXiv Detail & Related papers (2022-04-11T22:03:44Z) - Semantic Scaffolds for Pseudocode-to-Code Generation [47.09844589656143]
We propose a method for program generation based on semantic scaffolds, lightweight structures representing the high-level semantic and syntactic composition of a program.
By using semantic scaffolds during inference, we achieve a 10% absolute improvement in top-100 accuracy over the previous state-of-the-art.
arXiv Detail & Related papers (2020-05-12T17:10:13Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.