Regular papers

Pierluigi Ammirati, U Genova, Italy; Giorgio Delzanno, U Genova, Italy; Pierre Ganty, U Brussels (Libre), Belgium; Gilles Geeraerts, U Brussels (Libre), Belgium; Jean-François Raskin, U Brussels (Libre), Belgium; and Laurent Van Begin, U Brussels (Libre), Belgium
Babylon: An integrated toolkit for the specification and verification of parameterized systems

Alessandro Armando and Pasquale De Lucia, U Genova, Italy
Symbolic model-checking of linear programs

Benjamin Aziz and G. W. Hamilton, Dublin City U, Ireland
A privacy analysis for the π-calculus: The denotational approach

R. Corin and Sandro Etalle, U Twente, The Netherlands
An improved constraint-based system for the verification of security protocols

Fabio Martinelli, CNR Pisa, Italy
Symbolic partial model checking for security analysis

Natasha Sharygina and James C. Browne, U Texas-Austin, USA
Model checking large-scale software via abstraction of loop transitions