Process-Local Static Analysis of Synchronous Processes

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedings – Annual report year: 2018Researchpeer-review

View graph of relations

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.
Original languageEnglish
Title of host publicationStatic Analysis
PublisherSpringer
Publication date2018
Pages284-305
ISBN (Print)9783319997254
DOIs
Publication statusPublished - 2018
Event25th Static Analysis Symposium - Katholische Akademie , Freiburg im Breisgau, Germany
Duration: 29 Aug 201831 Aug 2018

Conference

Conference25th Static Analysis Symposium
LocationKatholische Akademie
CountryGermany
CityFreiburg im Breisgau
Period29/08/201831/08/2018
SeriesLecture Notes in Computer Science
Volume11002
ISSN0302-9743
CitationsWeb of Science® Times Cited: No match on DOI
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 152921196