\documentstyle{elsart}
\begin{document}

\begin{frontmatter}
\title{Static Analysis \\
Guest Editors' Introduction}
\author[1]{Agostino Cortesi}
\author[2]{Gilberto Fil\'e}
\address[1]{Univ. Ca' Foscari di Venezia, via Torino 155, 30153 Mestre-Venezia, Italy}
\address[2]{Univ. di Padova, via Belzoni 7, 35131 Padova, Italy}
\end{frontmatter}

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 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.
\end{document}
