Loading...
Please wait, while we are loading the content...
Similar Documents
Natural proofs for asynchronous programs using almost-synchronous reductions (2014)
| Content Provider | CiteSeerX |
|---|---|
| Author | Desai, Ankush Garg, Pranav Madhusudan, P. |
| Description | In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications 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. |
| File Format | |
| Language | English |
| Publisher Date | 2014-01-01 |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
