Erlang式并发的自动验证
Automatic Verification of Erlang-Style Concurrency
摘要：
提出了一种自动验证Erlang式高阶并发程序安全性的方法。受Core Erlang的启发，我们引入了Lambda-Actor，这是一种具有模式匹配代数数据类型的原型函数式语言，并增加了进程创建和异步消息传递原语。我们正式的抽象模型的λ-演员程序称为演员通信系统（ACS），它有一个自然的解释为一个矢量加法系统，其中一些验证问题是可判定的。我们给出了一个参数化的抽象解释框架，并使用它来构建一个多时间可计算的，基于流的，抽象语义的Lambda-Actor程序，然后我们使用它来引导ACS的建设，从而得出一个更准确的输入程序的抽象模型。我们已经构建了Soter，一个验证方法的工具实现，从而获得了第一个全自动的，无限状态的Erlang核心片段的模型检查器。我们发现，在实践中，我们的抽象技术是准确的，足以验证一个有趣的范围内的安全属性。虽然ACS的可覆盖性问题是Expspace完备的，但Soter可以非常有效地分析这些验证问题。
英文摘要：
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 have constructed Soter, a tool implementation of the verification method, thereby obtaining the first fully-automatic, infinite-state model checker for a core fragment of Erlang. 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 these verification problems surprisingly efficiently.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
