Static Analysis Guest editors’ introduction

Agostino Cortesi^{a} Gilberto Filé^{b}

a Univ. Ca’ Foscari di Venezia, via Torino 155, 30153 Mestre-Venezia, Italy b Univ. di Padova, via Belzoni 7, 35131 Padova, Italy

This special issue of Science of Computer Programming is dedicated to a selection of the best papers presented at the Static Analysis Symposium (SAS) held in 1999 in Venice, Italy.

Since 1994, SAS has been the annual conference and forum for researchers in all aspects of static analysis. SAS ’99 was the 6th edition of this series.

Already during the symposium, we found that some of the 18 papers of SAS ’99 had such original ideas and brought such important contributions that they deserved to be presented to a broader audience of computing science experts than that of the SAS partecipants. The Editors in Chief of “Science of Computer Programming” was enthusiastic about this idea and the present issue of the journal is the realization of our joint efforts.

To this end, seven of the contributions of SAS ’99 were selected, their authors were asked to submit an extended version of their work and in six cases this invitation was accepted and, after a thorough reviewing process, the articles contained in this volume were produced.

These articles give contributions to the area of static analysis that we consider particularly innovative and meaningful. Their contributions concern the foundations of static analysis as well as the design of useful and efficient abstract domains and the application of static analysis to Java and to mobile ambients. More precisely, the subjects studied in these works are as follows:

“Static analysis for eliminating unnecessary synchronisation from Java programs”, by J. Aldrich, C. Chambers, E.G. Sirer and S.Eggers shows how to use static analysis for eliminating up to 70 % of synchronization overhead from multi-threaded Java programs.

In “Binary decision graphs” by Laurent Mauborgne, the notion of binary decision diagrams is extended to binary decision graphs in order to model

Preprint submitted to Elsevier Science 13 July 2001

infinite boolean functions. Different classes of these graphs, corresponding to boolean functions of increasing complexity, are studied.

“Abstract interpretation of mobile ambients” by R.R.Hansen, J.G.Jensen, F. Nielson and H.Riis-Nielson, applies abstract interpretation to the ambient calculus, an extension of pi-calculus introduced by Cardelli and Gordon. The authors develop an analysis of ambient calculus that models which process can be inside what other processes.

The analysis of cryptographic protocols is tackled using tree automata and tree languages in “Abstracting cryptographic protocols with tree automata” by D. Monniaux. For the first time this paper uses abstract interpretation and in particular abstract model checking for the analysis of the protocols.

“State space reduction based on live variable anlysis” by M.Bozga, J-C. Fernandez and L. Ghirvu attaks the well-known state explosion in protocol specifications. The authors show that information about live variables allows important reductions in the state space.

A dead code analysis framework is described in “Eliminating dead code on recursive data” by Y.A.Liu and S.D.Stoller. This framework is based on general regular tree grammar. The analysis focuses on the identification of partially dead recursive data and is very precise and efficient.

We are grateful to all the authors for providing high-quality contributions. Finally, we thank all the reviewers for their helpful criticisms, suggestions and advice.