@inproceedings{10.1007/978-3-319-96142-2_23,
    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.},
    Address = {Cham},
    Author = {Bouajjani, Ahmed and Enea, Constantin and Ji, Kailiang and Qadeer, Shaz},
    BookTitle = {Computer Aided Verification},
    Editor = {Chockler, Hana and Weissenbacher, Georg},
    File = {On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony - Bouajjani2018\_Chapter\_OnTheCompletenessOfVerifyingMe (0) - a - a - p.pdf},
    ISBN = {978-3-319-96142-2},
    Pages = {372--391},
    Publisher = {Springer International Publishing},
    Title = {On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony},
    Year = {2018},
    date-added = {2019-09-05 13:48:05 +0200},
    date-modified = {2019-09-05 13:48:05 +0200},
    doi = {10.1007/978-3-319-96142-2_23}
}

@inproceedings{10.1007/978-3-319-96142-2_23, 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.}, Address = {Cham}, Author = {Bouajjani, Ahmed and Enea, Constantin and Ji, Kailiang and Qadeer, Shaz}, BookTitle = {Computer Aided Verification}, Editor = {Chockler, Hana and Weissenbacher, Georg}, File = {On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony - Bouajjani2018_Chapter_OnTheCompletenessOfVerifyingMe (0) - a - a - p.pdf}, ISBN = {978-3-319-96142-2}, Pages = {372--391}, Publisher = {Springer International Publishing}, Title = {On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony}, Year = {2018}, date-added = {2019-09-05 13:48:05 +0200}, date-modified = {2019-09-05 13:48:05 +0200}, doi = {10.1007/978-3-319-96142-2_23} }