Automatic Verification of Erlang-Style Concurrency (2013)

This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs automatically. Inspired by Core Erlang, we introduce Lambda-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 Lambda-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 Lambda-Actor and use it to build a polytime computable, flow-based, abstract semantics of Lambda-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.

@inproceedings{Soter:SAS13,
    author    = {E. D'Osualdo and J. Kochems and C.-H. L. Ong},
    title     = {Automatic Verification of {Erlang}-Style Concurrency},
    year      = {2013},
    booktitle = {Proceedings of the 20th Static Analysis Symposium},
    series    = {SAS'13},
    location  = {Seattle, USA},
    publisher = {Springer-Verlag}
}

@article{Soter:arXiv,
    author  = {E. D'Osualdo and J. Kochems and C.-H. L. Ong},
    title   = {Automatic Verification of {Erlang}-Style Concurrency},
    year    = {2013},
    note    = {Available at \url{http://arxiv.org/abs/1303.2201}},
    journal = {CoRR},
    volume  = {abs/1303.2201},
    ee      = {http://arxiv.org/abs/1303.2201},
}

Soter: An Automatic Safety Verifier for Erlang (2012)

This paper presents Soter, a fully-automatic program analyser and verifier for Erlang modules. The fragment of Erlang accepted by Soter includes the higher-order functional constructs and all the key features of actor concurrency, namely, dynamic spawning of processes and asynchronous message passing. Soter uses a combination of static analysis and infinite-state model checking to verify safety properties specified by the user. Given an Erlang module and a set of properties, Soter first extracts an abstract (approximate, sound) model in the form of an actor communicating system (ACS), and then checks if the properties are satisfied using a Petri net coverability checker, BFC. To our knowledge, Soter is the first fully-automatic, infinite-state model checker for a large fragment of Erlang. We find that in practice our abstraction technique is accurate enough to verify an interesting range of safety properties such as mutual-exclusion or boundedness of mailboxes. Though the ACS coverability problem is Expspace-complete, Soter can analyse these problems surprisingly efficiently.

@inproceedings{Soter:AGERE,
    author    = {D'Osualdo, Emanuele and Kochems, Jonathan and Ong, Luke},
    title     = {Soter: an Automatic Safety Verifier for {Erlang}},
    booktitle = {Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions},
    series    = {AGERE! '12},
    year      = {2012},
    location  = {Tucson, Arizona, USA},
    pages     = {137--140},
    url       = {http://doi.acm.org/10.1145/2414639.2414658},
    publisher = {ACM}
}