On the completeness of verifying message passing programs under bounded asynchrony

Ahmed Bouajjani; Constantin Enea; Kailiang Ji; Shaz Qadeer

doi:10.1007/978-3-319-96142-2_23

On the completeness of verifying message passing programs under bounded asynchrony

Ahmed Bouajjani
, Constantin Enea
, Kailiang Ji
, Shaz Qadeer

Université Paris 7
Microsoft Research

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

40 Citations (Scopus)

Résumé

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.

langue originale	Anglais
titre	Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
rédacteurs en chef	Georg Weissenbacher, Hana Chockler
Editeur	Springer Verlag
Pages	372-391
Nombre de pages	20
ISBN (imprimé)	9783319961415
Les DOIs	https://doi.org/10.1007/978-3-319-96142-2_23
état	Publié - 1 janv. 2018
Modification externe	Oui
Evénement	30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, Royaume-Uni Durée: 14 juil. 2018 → 17 juil. 2018

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10982 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
Pays/Territoire	Royaume-Uni
La ville	Oxford
période	14/07/18 → 17/07/18

Accès au document

10.1007/978-3-319-96142-2_23

Contient cette citation

Bouajjani, A., Enea, C., Ji, K., & Qadeer, S. (2018). On the completeness of verifying message passing programs under bounded asynchrony. Dans G. Weissenbacher, & H. Chockler (eds.), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (p. 372-391). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 10982 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-96142-2_23

Bouajjani, Ahmed ; Enea, Constantin ; Ji, Kailiang et al. / On the completeness of verifying message passing programs under bounded asynchrony. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Editeur / Georg Weissenbacher ; Hana Chockler. Springer Verlag, 2018. p. 372-391 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{32891fd31953496bb134296116a5474d,

title = "On the completeness of verifying message passing programs under bounded asynchrony",

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.",

author = "Ahmed Bouajjani and Constantin Enea and Kailiang Ji and Shaz Qadeer",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2018.; 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 14-07-2018 Through 17-07-2018",

year = "2018",

month = jan,

day = "1",

doi = "10.1007/978-3-319-96142-2\_23",

language = "English",

isbn = "9783319961415",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "372--391",

editor = "Georg Weissenbacher and Hana Chockler",

booktitle = "Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

}

Bouajjani, A, Enea, C, Ji, K & Qadeer, S 2018, On the completeness of verifying message passing programs under bounded asynchrony. Dans G Weissenbacher & H Chockler (eds), Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 10982 LNCS, Springer Verlag, p. 372-391, 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, Royaume-Uni, 14/07/18. https://doi.org/10.1007/978-3-319-96142-2_23

On the completeness of verifying message passing programs under bounded asynchrony. / Bouajjani, Ahmed; Enea, Constantin; Ji, Kailiang et al.
Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Ed. / Georg Weissenbacher; Hana Chockler. Springer Verlag, 2018. p. 372-391 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 10982 LNCS).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - On the completeness of verifying message passing programs under bounded asynchrony

AU - Bouajjani, Ahmed

AU - Enea, Constantin

AU - Ji, Kailiang

AU - Qadeer, Shaz

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-96142-2_23

DO - 10.1007/978-3-319-96142-2_23

M3 - Conference contribution

AN - SCOPUS:85051122068

SN - 9783319961415

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 372

EP - 391

BT - Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

A2 - Weissenbacher, Georg

A2 - Chockler, Hana

PB - Springer Verlag

T2 - 30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018

Y2 - 14 July 2018 through 17 July 2018

ER -

Bouajjani A, Enea C, Ji K, Qadeer S. On the completeness of verifying message passing programs under bounded asynchrony. Dans Weissenbacher G, Chockler H, rédacteurs en chef, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer Verlag. 2018. p. 372-391. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-96142-2_23

On the completeness of verifying message passing programs under bounded asynchrony

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation