2013 | OriginalPaper | Chapter
Automatic Verification of Erlang-Style Concurrency
Authors : Emanuele D’Osualdo, Jonathan Kochems, C. -H. Luke Ong
Published in: Static Analysis
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.