Automatic Verification of Erlang-Style Concurrency

This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs

automatically

. Inspired by Core Erlang, we introduce

λ

Actor

, a prototypical functional language with pattern-matching algebraic data types, augmented with process creation and asynchronous message-passing primitives. We formalise an abstract model of

λ

Actor

programs called

Actor Communicating System

(ACS) which has a natural interpretation as a vector addition system, for which some verification problems are decidable. We give a parametric abstract interpretation framework for

λ

Actor

and use it to build a polytime computable, flow-based, abstract semantics of

λ

Actor

programs, which we then use to bootstrap the ACS construction, thus deriving a more accurate abstract model of the input program.

We evaluate the method which we implemented in the prototype

Soter

. We find that in practice our abstraction technique is accurate enough to verify an interesting range of safety properties. Though the ACS coverability problem is

Expspace

-complete,

Soter

can analyse non-trivial programs in a matter of seconds.