Name
Abstract | ||
|---|---|---|
We present a tool that implements Owicki-Gries and relyguarantee methods for the compositional verification of multithreaded programs. Our tool computes the requisite auxiliary assertions automatically using an abstraction and refinement procedure. Our procedure is based on a Horn clause encoding of refinement queries and facilitates the discovery of thread-modular proofs when such proofs exist. We present the tool and its evaluation on a collection of benchmarks, including a direct comparison of the effectiveness of the proof rules. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-22110-1_32 | CAV |
Keywords | Field | DocType |
horn clause,requisite auxiliary assertion,refinement query,multithreaded program,relyguarantee method,direct comparison,proof rule,compositional verification,multi-threaded program,constraint-based verifier,refinement procedure,thread-modular proof | Abstraction,Programming language,Horn clause,Computer science,Algorithm,Multi threaded,Theoretical computer science,Mathematical proof,Encoding (memory) | Conference |
Citations | PageRank | References |
24 | 0.98 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ashutosh Gupta | 1 | 192 | 14.01 |
| Corneliu Popeea | 2 | 374 | 18.27 |
| Andrey Rybalchenko | 3 | 1439 | 68.53 |