Conference paper · Book chapter
Process-Local Static Analysis of Synchronous Processes
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.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2018 |
Pages: | 284-305 |
Proceedings: | 25th Static Analysis Symposium |
Series: | Lecture Notes in Computer Science |
Journal subtitle: | 25th International Symposium, Sas 2018, Freiburg, Germany, August 29–31, 2018, Proceedings |
ISBN: | 3319997246 , 3319997254 , 9783319997247 and 9783319997254 |
ISSN: | 03029743 and 16113349 |
Types: | Conference paper and Book chapter |
DOI: | 10.1007/978-3-319-99725-4_18 |
ORCIDs: | Nielson, Flemming and Nielson, Hanne Riis |