Name
Abstract | ||
|---|---|---|
This paper proposes a novel optimization of bounded model checking (BMC) for better run-time efficiency. Specifically, we define projections, an adaptation of dynamic program slices, and instruct the bounded model checker to check projections only. Given state properties over a subset of the program's variables, we prove the soundness of the proposed optimization. We propose a symbolic encoding of projections and implement it for a prototype language of concurrent programs. We have developed a tool called PBMC to evaluate the efficiency of the proposed approach. Our evaluation with various concurrent programs justifies the potential of projections to efficient verification. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-24953-7_26 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Model checking,Computer science,Slicing,Theoretical computer science,Soundness,Bounded function | Conference | 9364 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
6 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Habib Saissi | 1 | 8 | 4.23 |
| Péter Bokor | 2 | 29 | 5.14 |
| Neeraj Suri | 3 | 1040 | 112.91 |