A logic-based approach to data flow analysis problems
Lecture notes in computer sciencePublished 19 November 2005
Shmuel Sagiv, Nissim Francez, Michael Rodeh, Reinhard Wilhelm
Citations21
SJR quartileQ2
SJR score0.35
SNIP0.55
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A new uniform formalism for tracking static properties of programs with static assertions, i.e., assertions which hold independently of the specific execution path leading to this point.
Abstract
A new uniform formalism for tracking static properties of programs is presented. The formalism annotates each point in a program with static assertions, i.e., assertions which hold independently of the specific execution path leading to this point.The novel idea is to use Horn clauses to specify the consistent environments and the meaning of program operations.The abstract interpretation technique is used for finding conservative approximations to the static assertions and to analyze the accuracy of the approximation.The formalism is used to specify and solve the problem of tracking pointer equality and allocations in Pascal-like languages. It is shown that the solutions are optimal under some natural assumptions.
Keywords
Computer Science
Compilers: Principles, Techniques, and Tools
8,137 Citations1986Alfred V. Aho, Ravi Sethi +1 more
This book discusses the design of a Code Generator, the role of the Lexical Analyzer, and other topics related to code generation and optimization.
Abstract interpretation
6,131 Citations1977Patrick Cousot, Radhia Cousot
Foundations of Logic Programming
4,159 Citations1984John W. Lloyd
Systematic design of program analysis frameworks
1,598 Citations1979Patrick Cousot, Radhia Cousot
The systematic and correct design of program analysis frameworks with respect to a formal semantics is devoted to the main elements of the lattice theoretic approach to approximate semantic analysis of programs.
A unified approach to global program optimization
893 Citations1973Gary A. Kildall
A technique is presented for global analysis of program structure in order to perform compile time optimization of object code generated for expressions that includes constant propagation, common subexpression elimination, elimination of redundant register load operations, and live expression analysis.
IEEE Transactions on Software EngineeringTypestate: A programming language concept for enhancing software reliability
612 Citations1986Robert E. Strom, Shaula Yemini
The authors introduce a new programming language concept, called typestate, which is a refinement of the concept of type, which determines the subset of operations which is permitted in a particular context.
On the semantics of updates in databases
336 Citations1983Ronald Fagin, Jeffrey D. Ullman +1 more
A methodology for updating databases with integrity constraints and rules for deriving inexphcit information is suggested, which is adapted to updating databases, where different facts can carry different priorities, and to updating user views.
Journal of the ACMGlobal Data Flow Analysis and Iterative Algorithms
303 Citations1976John B. Kam, Jeffrey D. Ullman
Conditions under which the bound on the number of iterations required for propagation algorithms when the data is represented by bit vectors and depth-first ordering of the flow graph is used are considered are considered.
An efficient way to find the side effects of procedure calls and the aliases of variables
242 Citations1979John Banning
A precise inter-procedural data flow algorithm
210 Citations1981Eugene M. Myers
The avail, live, and must-summary data flow problems are shown to be NP-complete in the presence of aliasing and it is argued that in practice SET is small and on the order of the number of variables of the program.
Journal of the ACMA Fast and Usually Linear Algorithm for Global Flow Analysis
187 Citations1976Susan L. Graham, Mark N. Wegman
A new algorithm for global flow analysis on reducible graphs which has a worst-case time bound of O(e log e) function operations and a restriction to one-entry one-exit control structures guarantees linearity.
Constant propagation with conditional branches
132 Citations1985Mark N. Wegman, F. Kenneth Zadeck
The use of the algorithms presented here can result in smaller and faster compiled programs.
Updating Logical Databases.
130 Citations1984Ronald Fagin, Gabriel M. Kuper +2 more
A new approch to database updates is suggested, in which a database is treated as a collection of theories, and equivalence of databases under update operations is investigated.
ACM Computing SurveysElimination algorithms for data flow analysis
120 Citations1986Barbara G. Ryder, Marvin C. Paull
A unified model of a family of data flow algorithms, called elimination methods, is presented, which provides implementation-independent descriptions of the algorithms to facilitate comparisons among them and illustrate the sources of improvement in worst case complexity bounds.
Fast interprocedual alias analysis
115 Citations1989Keith D. Cooper, Ken Kennedy
A new algorithm for computing interprocedural aliases due to passing parameters by reference is presented and, when combined with algorithms for alias-free, flow-insensitive data-flow problems, yields algorithms for solution of the general flow- insensitive problems.
Analyzing aliases of reference formal parameters
86 Citations1985Keith D. Cooper
This paper presents a set of techniques for analyzing aliasing patterns, divided into detecting the introduction of aliases and tracking their propagation, and a data flow analysis framework is given for the propagation problem.
Lecture notes in computer scienceDelete operations and Horn formulas
3 Citations2005Rüdiger Schätz
Three delete operations, based on different heuristics, are studied, concerning propositional definite Horn formulas, which are increasingly complex in view of implementations and practical applications.