EC2 2014 SHORT PAPERS: PAPERS WITH ABSTRACTS

ABSTRACT. 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, which is sound and complete, 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 is 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.

ABSTRACT. We survey our research on concolic testing of concurrent programs. Based on concrete and symbolic executions of a concurrent program, our testing techniques derive inputs and schedules such that the execution space of the program under investigation is systematically explored. We will focus on con2colic testing which introduces interference scenarios. Interference scenarios capture the flow of data among different threads and enable a unified representation of path and interference constraints.

ABSTRACT. We developed a novel Functional Object-Oriented PARallel framework (FOOPAR) for analyzable high-level high-performance computing in Scala. Central to this framework are Distributed Memory Parallel Data structures, i.e., collections of data distributed in a shared nothing system together with parallel operations on these data.

In this position paper we shortly present FOOPAR’s design and focus on its properties w.r.t. analyzability and correctness. We prove the correctness and safety of one communication algorithm and show how specification testing (via ScalaCheck) can be used to bridge the gap between proof and implementation.