Static Analysis: 5th International Symposium, SAS'98, Pisa, Italy, September 14-16, 1998, Proceedings (Lecture Notes in Computer Science, 1503)

This volume contains the proceedings of the 1998 international symposium on staticanalysis(SAS'98)whichwasheldinPisa(Italy), onSeptember14-16,1998 and was part of a federated conference with ALP-PLILP'98 and several wo- shops. SAS'98isthe annualconferenceandforumforresearchersinallaspectsof staticanalysis. ItfollowstoSAS'94, SAS'95, SAS'96andSAS'97whichwereheld respectively in Namur (Belgium), Glasgow (UK), Aachen (Germany) and Paris (France), and the international workshops WSA'92 held in Bordeaux (France) and WSA'93 held in Padova (Italy). In response to the call for papers, 48 papers were submitted. All papers were reviewed by at least three reviewers and the program committee met in Pisa to select 20 papers based on the referee reports. There was a consensus at the meeting that the technical papers were of very high quality. In addition to the submitted papers, SAS'98 had a number of outstanding invited speakers. Roberto Giacobazzi, Peter Lee, Amir Pnueli, Dave Schmidt, Scott Smolka, and Bernhard Ste?en accepted our invitation to give invited talks or tutorials. Some ofthepapers(orabstracts)basedonthesetalksarealsoincludedin thisvolume. SAS'98 has been fortunate to rely on a number of individuals and orga- zations. I want to thank all the program committee members and referees, for their hard work in producing the reviews and for such a smooth and enj- able programcommittee meeting. Special thanks go to the conference chairman, Maurizio Gabbrielli, and to my students in Pisa who helped me a lot. More s- cial thanks go to Vladimiro Sassone, who made available to SAS'98 his excellent system for handling submissions and reviews on the web, and to Ernesto Lastres andRen` eMorenowhoweremy"systemmanagers". Static Analysis Foreword Program Committee of SAS'98 Contents Bidirectional Data Flow Analysis in Code Motion: Myth and Reality Motivation Related Work Preliminaries Code Motion in the Absence of Critical Edges Busy Code Motion Lazy Code Motion Code Motion in the Presence of Critical Edges Busy Code Motion Lazy Code Motion Conclusion References On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines Introduction Analysis of Subroutines Virtual Machine Values Instructions Operational Semantics Analysis Types Order among Types Target of Analysis Correctness of Analysis Example Returning to an Outer Caller Implementation Concluding Remark References Enabling Sparse Constant Propagation of Array Elements via Array SSA Form Introduction Array SSA Form Sparse Constant Propagation for Scalars and Array Elements Lattice Values for Scalar and Array Variables The Algorithm Sparse Conditional Constant Propagation Lattice Values of Executable Flags for Nodes and Edges Sparse Conditional Constant Propagation Algorithm Related Work Conclusions References Assessing the Effects of Flow-Sensitivity on Pointer Alias Analyses Introduction Analyses and Implementation Algorithms Implementation Results Description of Experiment Discussion Comparison with Other Results Efficiency Improvements Sharing Alias Sets Worklists Sorted Worklists ForwardBind Filtering Other Related Work Conclusions Acknowledgements References Analysis of Normal Logic Programs Introduction Preliminaries Normal Logic Programs and Constructive Negation Normal Forms in CET Depth (k) Analysis for Constructive Negation The Abstract Domain The Abstraction Function alpha c is a Congruence w.r.t. the H-Equivalence The Abstract Fixpoint Operator An Example Conclusion References The Correctness of Set-Sharing Introduction Equations and Substitutions Notation Substitutions Equations Variable-Idempotence Set-Sharing The Sharing Domain Abstract Operations for Sharing Sets Abstract Operations for Sharing Domains Discussion Soundness Idempotence Commutativity References Deriving Analysers by Folding/Unfolding of Natural Semantics and a Case Study: Slicing Introduction Natural Semantics Specification of a Slicing Property Derivation of the Dynamic on the Fly Analyser Related Work Conclusion References A Symbolic Semantics for Abstract Model Checking Introduction Concrete Model Checking Abstract Interpretation Theory The Symbolic Graph Symbolic Model Checking Abstract Model Checking About Optimality Related Works Conclusions References Appendix Automatic Determination of Communication Topologies in Mobile Systems Introduction Mobile Systems in the pi-Calculus Nonstandard Semantics of Mobile Systems Abstract Interpretation of Mobile Systems Design of a Computable Analysis Conclusion References Constructing Specific SOS Semantics for Concurrency via Abstract Interpretation Introduction The concrete domain The abstract domain Rule-based inductive de nitions The concrete domain FP The abstract domain FC The abstract interpretation function A fragment of a hierarchy The abstract domain FI The abstraction from proved to interleaving transition systems The abstraction from causal to interleaving transition systems The hierarchy Conclusions References A First-Order Language for Expressing Aliasing and Type Properties of Logic Programs Introduction Preliminaries Regular term grammars A language of properties A proof procedure for L Applications Conclusions References Refining Static Analyses by Trace-Based Partitioning Using Control Flow Introduction Trace-Based Partitioning Using Control Flow Concrete Semantics Collecting Semantics Set of Labeled Abstract Property Domain Abstract Operations Abstract Semantics Complexity and Precision Finite Sets of Labeled Convex Polyhedra Convex Polyhedra Domain Specific Functions Example Finite Sets of Labeled Linear Congruences Linear Congruence Domain Lifting the Domain of Linear Congruences Example Conclusions and Further Work References Building Complete Abstract Interpretations in a Linear Logic-Based Setting Introduction Basic Notions Completeness Problems in Abstract Interpretations Quantales and Solutions to Completeness Problems The Case of Unital Commutative Quantales An Application in Data Structure Completeness Complete Semantics for Logic Program Analysis Notation TP-Completeness Complete Semantics for Groundness Analysis On the Power of Homeomorphic Embedding for Online Termination Introduction Well-Quasi Orders and Homeomorphic Embedding Comparing wbr's and wfo's General Comparison Homeomorphic Embedding and Monotonic Wfo's Discussion and Conclusion Small Experiments with the ECCE System Analysis of Imperative Programs through Analysis of Constraint Logic Programs Introduction Analysis through Semantics Big-Step and Small-Step Semantics One-State and Two-State Semantics Analysis of the Semantics A Semantics-Based Interpreter Structural Operational Semantics Partial Evaluation Representation of Imperative Programs Control of Partial Evaluation Results Related Work Final Remarks References Improving Control in Functional Logic Program Specialization Introduction Preliminaries The Generalized Specialization Algorithm Improving Control of NPE Local Control Global Control Experiments Discussion References Directional Type Inference for Logic Programs Introduction Abstractions Directional Types and Type Programs Directional Type Inference Complexity of Directional Type Checking Future work References Finite Subtype Inference with Explicit Polymorphism Introduction Type System Type Inference Containment and Entailment Finite Satisfiability Scoping of Type Variables Correctness of Type Inference Conclusions Sparse Jacobian Computation in Automatic Differentiation by Static Program Analysis Introduction Automatic Differentiation (AD) Sparse Jacobian Analysis Problem Statement Array Regions Analysis A Descriptor for Trapezoidal Matrices Computing the Differentiation Dependence Graph (DDG) Data Structure Selection and Conflicts Resolving Choice of Data Structure Conflicts Resolving Derivative Code Generation Declarations Initializations Experimental Results Odyssée Some Comparison Tests Conclusion References A New Solution to the Hidden Copy Problem Introduction Motivation An Unrealized Analytic Approach A Dynamic Approach that didn't Work Basis for a Solution Outline of the Paper Language Copy/Value Semantics Lazy Copy Semantics Optimized Lazy Copy Semantics Must-Alias Analysis Notation Abstract Interpretation Algorithm Copy Optimization Transformation Applications Conclusions and Future Work References A Tutorial on Domain Theory in Abstract Interpretation Program Analysis as Model Checking of Abstract Interpretations Motivation Iterative Flow Analysis Model Checking Operational Semantics and Abstractions Simulations Collecting Semantics An Analysis Methodology Discussion Conclusion References Certifying, Optimizing Compilation Author Index

This book constitutes the refereed proceedings of the 5th International Symposium on Static Analysis, SAS'98, held in Pisa, Italy, in September 1998.
The 20 revised full papers presented were carefully reviewed and selected from a total of 48 submissions. Also included is an invited tutorial. The papers are organized in topical sections on data-flow analysis, logic programming, concurrency, abstract domains, partial evaluation, type inference, and optimization. The invited tutorial by David Schmidt and Bernhard Steffen is entitled "data-flow analysis as model checking of abstract interpretations".

This book constitutes the refereed proceedings of the 5th International Symposium on Static Analysis, SAS'98, held in Pisa, Italy, in September 1998. The 20 revised full papers presented were carefully reviewed and selected from a total of 48 submissions. Also included is an invited tutorial. The papers are organized in topical sections on data-flow analysis, logic programming, concurrency, abstract domains, partial evaluation, type inference, and optimization. The invited tutorial by David Schmidt and Bernhard Steffen is entitled "data-flow analysis as model checking of abstract interpretations." This text constitutes the proceedings of the 5th International Symposium on Static Analysis held in September 1998. The papers presented are organized into topical sections on data flow analysis, logic programming, concurrency, abstract domains, partial evaluation, type inference and optimization.