Natural proofs for asynchronous programs using almost-synchronous reductions

We consider the problem of provably verifying that an asyn-chronous message-passing system satisfies its local asser-tions. We present a novel reduction scheme for asynchronous event-driven programs that finds almost-synchronous invari-ants — invariants consisting of global states where mes-sage buffers are close to empty. The reduction finds almost-synchronous invariants and simultaneously argues that they cover all local states. We show that asynchronous programs often have almost-synchronous invariants and that we can exploit this to build natural proofs that they are correct. We implement our reduction strategy, which is sound and com-plete, and show that it is more effective in proving programs correct as well as more efficient in finding bugs in several programs, compared to current search strategies which al-most always diverge. The high point of our experiments is that our technique can prove the Windows Phone USB Driver written in P [9] correct for the responsiveness prop-erty, which was hitherto not provable using state-of-the-art model-checkers