Automatic Verification of Erlang−Style Concurrency
Emanuele D'Osualdo‚ Jonathan Kochems and Luke Ong
Abstract
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. Thus ACS enjoys decidable coverability and LTL model checking problems. We give a general abstract interpretation framework for λActor progr
Details
| Institution |
University of Oxford DCS Technical Report |
| Note | |
| Year |
2012 |
Links
Related pages
|
People |