Name
Abstract | ||
|---|---|---|
Automatic verification of concurrent programs written in low-level languages like ANSI-C is an important task as multi-core architectures are gaining widespread adoption. Formal verification, although very valuable for this domain, rapidly runs into the state-explosion problem due to multiple thread interleavings. Recently, Bounded Model Checking (BMC) has been used for this purpose, which does not scale in practice. In this work, we develop a method to further constrain the search space for BMC techniques using underapproximations of data flow of shared memory and lazy demand-driven refinement of the approximation. A novel contribution of our method is that our underapproximation is guided by likely data-flow invariants mined from dynamic analysis and our refinement is based on proof-based learning. We have implemented our method in a prototype tool. Initial experiments on benchmark examples show potential performance benefit. |
Year | Venue | Field |
|---|---|---|
2017 | ATVA | Programming language,Model checking,Shared memory,Computer science,Thread (computing),Theoretical computer science,Invariant (mathematics),Formal verification,Data flow diagram,Bounded function |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
5 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sumanth Prabhu | 1 | 0 | 0.34 |
| Peter Schrammel | 2 | 134 | 19.10 |
| Mandayam Srivas | 3 | 2 | 1.86 |
| Michael Tautschnig | 4 | 425 | 25.84 |
| Anand Yeolekar | 5 | 86 | 5.49 |