Process-Local Static Analysis of Synchronous Processes

被引：10

作者：

Midtgaard, Jan ^{[1
]}

Nielson, Flemming ^{[2
]}

Nielson, Hanne Riis ^{[2
]}

机构：

[1] Univ Southern Denmark, Maersk Mc Kinney Moller Inst, Odense, Denmark

[2] Tech Univ Denmark, DTU Compute, Lyngby, Denmark

来源：

STATIC ANALYSIS (SAS 2018) | 2018年 / 11002卷

关键词：

MOBILE; DERIVATIVES; SYSTEM;

D O I：

10.1007/978-3-319-99725-4_18

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We develop a modular approach to statically analyse imperative processes communicating by synchronous message passing. The approach is modular in that it only needs to analyze one process at a time, but will in general have to do so repeatedly. The approach combines lattice-valued regular expressions to capture network communication with a dedicated shuffle operator for composing individual process analysis results. We present both a soundness proof and a prototype implementation of the approach for a synchronous subset of the Go programming language. Overall our approach tackles the combinatorial explosion of concurrent programs by suitable static analysis approximations, thereby lifting traditional sequential analysis techniques to a concurrent setting.

引用

页码：284 / 305

页数：22