Name
Title | ||
|---|---|---|
Early Results with Precision Abstraction: Using Data-flow Analysis to Improve the Scalability of Model Checking |
Abstract | ||
|---|---|---|
This paper presents a new state space reduction technique that applies to model checking of software. The new technique, precision abstraction, borrows ideas from dataflow analysis to identify procedures that can be analyzed context-insensitively without affecting the accuracy of the verification of a given property. These context-insensitive procedures can then be represented with fewer states than would be needed context-sensitive analysis. Preliminary results indicate that the number of transitions in the analysis prescribed by our approach is at least 155 times fewer than the exhaustive analysis a model checker would otherwise perform. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1109/IPDPS.2007.370520 | Long Beach, CA |
Keywords | Field | DocType |
data flow analysis,program verification,context-sensitive analysis,data-flow analysis,model checking,precision abstraction,software verification,state space reduction technique | Abstraction model checking,Model checking,Computer science,Parallel computing,Data-flow analysis,Dataflow,Software,Software measurement,Software verification,Scalability | Conference |
ISBN | Citations | PageRank |
1-4244-0910-1 | 0 | 0.34 |
References | Authors | |
13 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Adam Brown | 1 | 0 | 0.34 |
| James C. Browne | 2 | 998 | 300.57 |
| Calvin Lin | 3 | 89 | 12.04 |