Delta execution for efficient state-space exploration of object-oriented programs
Abstract
State-space exploration is the essence of model checking and an increasingly popular approach for automating test generation. A key issue in exploration of object-oriented programs is handling the program state, in particular the heap. Previous research has focused on standard program execution that operates on one state/heap. We present Delta Execution, a technique that simultaneously operates on several states/heaps. It exploits the fact that many execution paths in state-space exploration partially overlap and speeds up the exploration by sharing the common parts across the executions and separately executing only the "deltas" where the executions differ.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
The number of tests needed to evaluate every possible value pair can be significantly smaller than the exhaustive testing alternative.
“The number of tests needed to evaluate every possible value pair can be significantly smaller than the exhaustive testing alternative since each test can simultaneously contribute to multiple value pairs [22, 44, 80].”
From Fairness testing: testing software for discrimination (2017) · cites this paper as [22]
The citation lists haven’t been fetched yet
References 57 · Cited by 26
- Authors
- d'Amorim, M., Lauterburg, S., & Marinov, D.
- Affiliations
- University of Illinois at Urbana-Champaign
- University of Illinois Urbana-Champaign (US)
- ORCID
- Marinov, Darko
- Venue
- Proceedings of the 2007 international symposium on Software testing and analysis
- Publisher
- ACM
- Published
- 2007-07-09
- Pages
- 50-60
- OpenAlex
- W2145212015
- Cited by
- 26
- References
- 57
- Citations by year
- 2021: 1 · 2018: 2 · 2017: 2 · 2016: 1 · 2014: 2 · 2013: 4
- FWCI
- 2.26
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- International Symposium on Software Testing and Analysis (publishedVersion)
- Funders
- National Science Foundation
- Microsoft Research
- Topics
- Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
- Keywords
- state space exploration, object-oriented software, model checking, test case generation, heap management
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review