Taming Unboundedness in Concurrent Program Analysis

Emanuele D'Osualdo

The focus of this talk is on automatic analysis for message passing based concurrent systems.
First, I will give a brief overview of Soter, an analysis framework for the Erlang programming language. The analysis combines abstract interpretation with infinite-state model checking to be able to prove safety properties such as control location unreachability, mutual exclusion, bounds on message buffers. The analysis needs to carefully abstract unbounded resources that are built in the concurrency model, namely dynamically created threads and unbounded message buffers for asynchronous communication.
Soter handles these features with so-called counter abstraction, which for threads results in a rather crude abstraction. I will explain the consequences of the issue and an approach to solve it using the notion of depth-boundedness in the pi-calculus. The solution provides a more flexible and precise abstraction of concurrency, retaining decidability of the analysis. While the formalism of choice is the pi-calculus, the concepts involved are of general interest and I will not assume particular familiarity with it.
Time permitting, I will sketch how depth-boundedness can be adapted for verifying security protocols.