Title: Parallel Bug-finding in Concurrent Programs via Reduced Interleaving Instances

Speaker: Peter Schrammel    (bio) (bio)

Peter Schrammel is CTO and co-founder of Diffblue. He is also an Assistant Professor of Computer Science at the University of Sussex. His research interests lie in formal methods for building dependable systems and understanding complex systems. In particular, his interests include program analysis algorithms combining abstract interpretation and decision procedures, acceleration and strategy iteration methods for efficient and precise invariant inference, incremental solving and abstraction refinement, and verification and testing of cyber-physical systems.

When: Tuesday, 01 March 2022 at 1900 hrs (IST)     

Abstract:
Concurrency poses a major challenge for program verification, but it can also offer an opportunity to scale when subproblems can be analysed in parallel. We exploit this opportunity here and use a parametrizable code-to-code translation to generate a set of simpler program instances, each capturing a reduced set of the original program's interleavings. These instances can then be checked independently in parallel. Our approach does not depend on the tool that is chosen for the final analysis, is compatible with weak memory models, and amplifies the effectiveness of existing tools, making them find bugs faster and with fewer resources. We use Lazy-CSeq as an off-the-shelf final verifier to demonstrate that our approach is able, already with a small number of cores, to find bugs in the hardest known concurrency benchmarks in a matter of minutes, whereas other dynamic and static tools fail to do so in hours.