Title
Scaling Model Checking for Test Generation Using Dynamic Inference
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 Yeolekar1865.49
Divyesh Unadkat241.09
Vivek Agarwal314527.82
Shrawan Kumar49010.04
R. Venkatesh530.41