scholarly journals Data flow analysis as model checking

1990 ◽  
Vol 19 (325) ◽  
Author(s):  
Bernhard Steffen
Keyword(s):  
Model Checking ◽  
Modal Logic ◽  
Data Flow ◽  
Flow Analysis ◽  
Specific Model ◽  
Specification Language ◽  
Model Checker ◽  
Modal Formula ◽  
Data Flow Analysis ◽  
Flow Graphs

The paper develops the idea that modal logic provides an appropriate framework for the specification of data flow analysis (DFA) algorithms as soon as programs are represented as models of the logic. This can be exploited to construct a DFA-<strong>generator</strong> that generates efficient DFA-algorithms from modal specifications by partially evaluating a specific model checker wrt the specifying modal formula. Moreover, the use of a modal logic as specification language for DFA-algorithms supports the compositional development of specifications and structured proofs of properties of DFA-algorithms. These ideas are applied to the problem of determining optimal computation points within flow graphs.

scholarly journals Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow Analysis

2020 ◽  
pp. 112-140 ◽  
Author(s):  
Krishnendu Chatterjee ◽  
Amir Kafshdar Goharshady ◽  
Rasmus Ibsen-Jensen ◽  
Andreas Pavlogiannis
Keyword(s):  
Data Flow ◽  
Flow Analysis ◽  
Demand Analysis ◽  
Finite Domain ◽  
Data Flow Analysis ◽  
On Demand ◽  
Time Optimal ◽  
Speed Up ◽  
Flow Functions ◽  
Flow Graphs

AbstractInterprocedural data-flow analyses form an expressive and useful paradigm of numerous static analysis applications, such as live variables analysis, alias analysis and null pointers analysis. The most widely-used framework for interprocedural data-flow analysis is IFDS, which encompasses distributive data-flow functions over a finite domain. On-demand data-flow analyses restrict the focus of the analysis on specific program locations and data facts. This setting provides a natural split between (i) an offline (or preprocessing) phase, where the program is partially analyzed and analysis summaries are created, and (ii) an online (or query) phase, where analysis queries arrive on demand and the summaries are used to speed up answering queries.In this work, we consider on-demand IFDS analyses where the queries concern program locations of the same procedure (aka same-context queries). We exploit the fact that flow graphs of programs have low treewidth to develop faster algorithms that are space and time optimal for many common data-flow analyses, in both the preprocessing and the query phase. We also use treewidth to develop query solutions that are embarrassingly parallelizable, i.e. the total work for answering each query is split to a number of threads such that each thread performs only a constant amount of work. Finally, we implement a static analyzer based on our algorithms, and perform a series of on-demand analysis experiments on standard benchmarks. Our experimental results show a drastic speed-up of the queries after only a lightweight preprocessing phase, which significantly outperforms existing techniques.

scholarly journals Data-Flow Analysis as Model Checking Within the jABC

2006 ◽  
pp. 101-104 ◽  
Author(s):  
Anna-Lena Lamprecht ◽  
Tiziana Margaria ◽  
Bernhard Steffen
Keyword(s):  
Model Checking ◽  
Data Flow ◽  
Flow Analysis ◽  
Data Flow Analysis

Combining Model Checking and Data-Flow Analysis

2018 ◽  
pp. 493-540 ◽  
Author(s):  
Dirk Beyer ◽  
Sumit Gulwani ◽  
David A. Schmidt
Keyword(s):  
Model Checking ◽  
Data Flow ◽  
Flow Analysis ◽  
Data Flow Analysis

scholarly journals Abstract Interpretation in the Operational Semantics Hierarchy

1997 ◽  
Vol 4 (2) ◽  
Author(s):  
David A. Schmidt
Keyword(s):  
Model Checking ◽  
Abstract Interpretation ◽  
Data Flow ◽  
Flow Analysis ◽  
Operational Semantics ◽  
Second Order ◽  
Analysis Model ◽  
Small Step ◽  
Data Flow Analysis ◽  
First Order

We systematically apply the principles of Cousot-Cousot-style abstract interpretation (a.i.) to the hierarchy of operational semantics definitions - flowchart, big-step, and small-step semantics. For each semantics format we examine the principles of safety and liveness interpretations, first-order and second-order analyses, and termination properties. Application of a.i. to data-flow analysis, model checking, closure analysis, and concurrency theory are demonstrated. Our primary contributions are separating the concerns of safety, termination, and efficiency of representation and showing how a.i. principles apply uniformly to the various levels of the operational semantics hierarchy and their applications.

Sign in / Sign up

Export Citation Format

Share Document