Abstract | ||
---|---|---|
Model checking engines employed to generate test cases covering the structure of the model or code are limited by factors like code size, loops and floating point computation. We propose an approach that overcomes these limitations by approximating code fragments by dynamically inferring their post-conditions. We use Daikon to infer likely invariants from execution traces, which are used as post conditions to compactly represent the state space computed by these code fragments. The resulting approximation enables application-level test case generation over larger code sizes using model checking, given the same resources of time, memory and computing power. Case studies show the efficacy of this approach. |
Year | DOI | Venue |
---|---|---|
2013 | 10.1109/ICST.2013.29 | Software Testing, Verification and Validation |
Keywords | Field | DocType |
application-level test case generation,larger code size,approximating code fragment,model checking,scaling model checking,code fragment,test generation,computing power,dynamic inference,code size,case study,test case,model checking engine,computational modeling,indexes,scalability,formal verification | Abstraction model checking,Model checking,Floating point,Computer science,Parallel computing,Algorithm,Test case,State space,Computation,Scalability,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-4673-5961-0 | 3 | 0.41 |
References | Authors | |
15 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Anand Yeolekar | 1 | 86 | 5.49 |
Divyesh Unadkat | 2 | 4 | 1.09 |
Vivek Agarwal | 3 | 145 | 27.82 |
Shrawan Kumar | 4 | 90 | 10.04 |
R. Venkatesh | 5 | 3 | 0.41 |