Name
Abstract | ||
|---|---|---|
Software model checking is the process of systematically exploring a program's state space to find hard-to-discover errors. Because of the exponential size of the state space, an exhaustive search of the state space is often impossible given the memory resources. In such cases, an estimate of how much of the state space is covered can help the verifier to decide whether to employ additional computational resources or to use more aggressive abstraction techniques. Our work focuses on coverage estimation for explicit-state model checking of software programs. In this paper, we present an estimation algorithm that is based on Monte Carlo techniques that sample the unexplored portion of the reachability graph. We implemented our algorithm in Java Pathfinder and evaluated our approach on a suite of Java programs, simulating out-of-memory errors after a known percentage of a program's state space had been searched. Our empirical studies show that, on average, our algorithm's coverage estimates differ from the actual coverage by less than 10 percentage points, with a standard deviation of about 5 percentage points - regardless of whether the actual state-space coverage is low (3%) or high (95%). |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/ASE.2009.24 | Auckland |
Keywords | Field | DocType |
Java,Monte Carlo methods,data flow analysis,formal specification,program verification,reachability analysis,Java Pathfinder,Java programs,Monte Carlo techniques,aggressive abstraction techniques,computational resources,estimation algorithm,explicit-state model checking,hard-to-discover errors,memory resources,out-of-memory errors,reachability graph,software model checking,software programs,state-space coverage estimation,Model checking,automatic verification,coverage estimation | Model checking,Brute-force search,Computer science,Data-flow analysis,Theoretical computer science,Reachability,Memory management,Percentage point,Standard deviation,State space | Conference |
ISSN | ISBN | Citations |
1938-4300 E-ISBN : 978-0-7695-3891-4 | 978-0-7695-3891-4 | 1 |
PageRank | References | Authors |
0.36 | 15 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Taleghani, A. | 1 | 1 | 0.36 |
| Joanne M. Atlee | 2 | 1 | 0.36 |