Effect-driven Flow Analysis

Research output: Chapter in Book/Report/Conference proceedingConference paper

4 Citations (Scopus)
15 Downloads (Pure)


Traditional machine-based static analyses use a worklist algorithm to explore the analysis state space, and compare each state in the worklist against a set of seen states as part of their fixed-point computation. This may require many state comparisons, which gives rise to a computational overhead. Even an analysis with a global store has to clear its set of seen states each time the store updates because of allocation or side-effects, which results in more states being reanalyzed and compared.
In this work we present a static analysis technique, ModF, that does not rely on a set of seen states, and apply it to a machine-based analysis with global-store widening. Modf analyzes one function execution at a time to completion while tracking read, write, and call effects. These effects trigger the analysis of other function executions, and the analysis terminates when no new effects can be discovered.
We compared Modf to a traditional machine-based analysis implementation on a set of 20 benchmark programs and found that Modf is faster for 17 programs with speedups ranging between 1.4x and 12.3x. Furthermore, Modf exhibits similar precision as the traditional analysis on most programs and yields state graphs that are comparable in size.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings
EditorsRuzica Piskac, Constantin Enea
Number of pages28
ISBN (Electronic)978-3-030-11245-5
ISBN (Print)978-3-030-11244-8
Publication statusPublished - 13 Jan 2019
Event20th International Conference on Verification, Model Checking, and Abstract Interpretation - Cascais, Portugal
Duration: 13 Jan 201915 Jan 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11388 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference20th International Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated titleVMCAI 2019


  • Abstract interpretation
  • Effects
  • Program analysis
  • Static analysis


Dive into the research topics of 'Effect-driven Flow Analysis'. Together they form a unique fingerprint.

Cite this