SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Fri 24 Oct 2014 11:37 - 12:00 at Salon E - Specification and Verification Chair(s): Gary Leavens

We consider the problem of provably verifying that an asynchronous message-passing system satisfies its local assertions. We present a novel reduction scheme for asynchronous event-driven programs that finds almost-synchronous invariants – invariants consisting of global states where message 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 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 almost always diverge. The high point of our experiments show that our technique can prove the Windows Phone USB Driver written in P correct for the receptiveness property, which was hitherto not provable using state-of-the-art model-checkers.

Fri 24 Oct

oopsla2014
10:30 - 12:00: OOPSLA - Specification and Verification at Salon E
Chair(s): Gary Leavens University of Central Florida
oopsla2014141413940000010:30 - 10:52
Talk
Nicolás RosnerDept. of Computer Science FCEyN, University of Buenos Aires, Valeria BengoleaDept. of Computer Science FCEFQyN, University of Rio Cuarto, Pablo PonzioDept. of Computer Science FCEFQyN, University of Rio Cuarto, Shadi Abdul KhalekGoogle, Nazareno AguirreDept. of Computer Science FCEFQyN, University of Rio Cuarto, Marcelo F. FriasDept. of Software Engineering Instituto Tecnológico de Buenos Aires, Sarfraz KhurshidUniversity of Texas at Austin
Link to publication
oopsla2014141414075000010:52 - 11:15
Talk
Link to publication
oopsla2014141414210000011:15 - 11:37
Talk
Aaron TuronMPI-SWS, Viktor VafeiadisMPI-SWS, Germany, Derek DreyerMPI-SWS
Link to publication
oopsla2014141414345000011:37 - 12:00
Talk
Ankush DesaiUniversity of California, Berkeley, Pranav GargUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign
Link to publication