Modular Static Analysis of Actor Programs

Research output: Unpublished contribution to conferenceUnpublished abstract

55 Downloads (Pure)


Existing static analyses for actor programs ex- plicitely model all possible execution interleavings. Because the number of interleavings increases exponentially with the number of actors and messages exchanged, such analyses scale poorly. We describe the first modular analysis for actor programs, that analyzes each actor in separation of each other. This analysis over-approximate over the diferent interleavings without explicitly modeling them, rendering it scalable. We demonstrate its enhanced scalability by comparing the analysis of the Savina benchmark suite with a non-modular analysis and our new modular analysis. Our technique succeeds in analyzing all of the Savina benchmarks in a matter of seconds, while the non-modular analysis times out on more than half of these benchmarks. Moreover, we show that the precision of our modular remains on par with the precision of the non-modular analysis.
Original languageEnglish
Number of pages5
Publication statusPublished - 5 Dec 2017
EventBElgian-NEtherlands eVOLution seminar 2017 - Antwerpen, Belgium, Antwerpen, Belgium
Duration: 4 Dec 20175 Dec 2017
Conference number: 16


ConferenceBElgian-NEtherlands eVOLution seminar 2017
Abbreviated titleBENEVOL
Internet address


  • abstract interpretation
  • actors
  • static analysis
  • modular analysis


Dive into the research topics of 'Modular Static Analysis of Actor Programs'. Together they form a unique fingerprint.

Cite this