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.

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 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

scholarly journals Interprocedural Control Flow Analysis (Extended version)

1998 ◽  
Vol 27 (538) ◽  
Author(s):  
Flemming Nielson ◽  
Hanne Riis Nielson
Keyword(s):  
Abstract Interpretation ◽  
Data Flow ◽  
Flow Analysis ◽  
Object Oriented ◽  
Control Flow ◽  
Data Flow Analysis ◽  
Context Sensitive ◽  
Mutable State ◽  
Do So ◽  
Control Flow Analysis

Control Flow Analysis is a widely used approach for analysing functional and object oriented programs and recently it has also successfully been used to analyse more challenging notions of computation involving concurrency. However, once the applications become more demanding also the analysis needs to be more precise in its ability to deal with mutable state (or side-effects) and to perform polyvariant (or context-sensitive) analysis. Several insights in Data Flow Analysis and Abstract Interpretation show how to do so for imperative programs but the techniques have not had much impact on Control Flow Analysis because of the less abstract way in which the techniques are normally expressed. In this paper we show how to incorporate a number of key insights from Data Flow Analysis involving such advanced interprocedural techniques as call strings and assumption sets using Abstract Interpretation to induce the analyses from a general collecting semantics.

scholarly journals Semantic Foundations of Data Flow Analysis

1981 ◽  
Vol 10 (131) ◽  
Author(s):  
Flemming Nielson
Keyword(s):  
Program Analysis ◽  
Abstract Interpretation ◽  
Data Flow ◽  
Flow Analysis ◽  
Denotational Semantics ◽  
System Of Equations ◽  
Program Transformations ◽  
Sensitive Data ◽  
Data Flow Analysis ◽  
Made In

<p>Abstract Interpretation (P. Cousot, R. Cousot and others) is a method for program analysis that is able to describe many data flow analyses. We investigate and weaken the assumptions made in abstract interpretation and express abstract interpretation within Denotational Semantics. As an example we specify constant propagation.</p><p>Some authors have used abstract interpretation to formulate ''available expressions'' (a so-called ''history-sensitive'' data flow analysis). Our development of ''available expressions'' is better justified, semantically.</p><p>In traditional data flow analysis and abstract interpretation it is generally assumed that the ''Meet Over all Paths'' solution is wanted. We prove that the solution specified by our approach is the ''Meet Over all Paths'' solution to a certain system of equations obtained from the program.</p><p>To indicate the usefulness of our approach we show how to validate a class of program transformations, including ''constant folding''.</p><p>Throughout this paper we use a toy language consisting of declarations, expressions and commands (involving conditional and iteration). Excluded are procedures and jumps.</p>

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
Sign in / Sign up

Export Citation Format

Share Document