@inbook{50e72a2c4ee440b09997ed15d7b04051,
title = "Structurally Defined Conditional Data-Flow Static Analysis",
abstract = " Data flow analysis (DFA) is an important verification technique that computes the effect of data values propagating over program paths. While more precise than flow-insensitive analyses, such an analysis is time-consuming. This paper investigates the acceleration of DFA by structural decomposition of the underlying control flow graph. Specifically, we explore the cost and effectiveness of dividing program paths into subsets by partitioning path suffixes at conditional statements, applying a DFA on each subset, and then combining the resulting invariants. This yields a family of independent DFA problems that are solved in parallel and where the partial results of each problem represent safe program invariants. Empirical evaluations reveal that depending on the DFA type and its conditional implementation the invariants for a large fraction of program points can be computed in less time than traditional DFA. This work suggests a strategy for an “anytime DFA” algorithm: computing safe program invariants as the analysis proceeds. ",
author = "Elena Sherman and Dwyer, {Matthew B.}",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2018.; 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 ; Conference date: 14-04-2018 Through 20-04-2018",
year = "2018",
month = jan,
day = "1",
doi = "10.1007/978-3-319-89963-3_15",
language = "American English",
isbn = "9783319899626",
series = "0302-9743",
publisher = "Springer Verlag",
pages = "249--265",
editor = "Dirk Beyer and Marieke Huisman",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 Thessaloniki, Greece, April 14-20, 2018",
address = "Germany",
}