Name
Abstract | ||
|---|---|---|
We address the problem of verifying message passing programs, defined as a set of processes communicating through unbounded FIFO buffers. We introduce a bounded analysis that explores a special type of computations, called k-synchronous. These computations can be viewed as (unbounded) sequences of interaction phases, each phase allowing at most k send actions (by different processes), followed by a sequence of receives corresponding to sends in the same phase. We give a procedure for deciding k-synchronizability of a program, i.e., whether every computation is equivalent (has the same happens-before relation) to one of its k-synchronous computations. We show that reachability over k-synchronous computations and checking k-synchronizability are both PSPACE-complete. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-96142-2_23 | COMPUTER AIDED VERIFICATION, CAV 2018, PT II |
DocType | Volume | ISSN |
Conference | 10982 | 0302-9743 |
Citations | PageRank | References |
1 | 0.35 | 21 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| A. Bouajjani | 1 | 344 | 31.93 |
| Constantin Enea | 2 | 249 | 26.95 |
| Kailiang Ji | 3 | 1 | 0.68 |
| Shaz Qadeer | 4 | 3257 | 239.11 |