On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony

Ahmed Bouajjani, Constantin Enea, Kailiang Ji +1

We address the problem of verifying message passing programs, defined as a set of parallel processes communicating through unbounded FIFO buffers. We introduce a bounded analysis t…