Regular papers

Andrew W. Appel, Princeton U, USA; Neophytos G. Michael, Princeton U, USA; Aaron Stump, Stanford U, USA; and Roberto Virga, Princeton U, USA
A trustworthy proof checker

Alessandro Armando and Luca Compagna, U Genova, Italy
Automatic SAT-compilation of security problems

Ernie Cohen, Microsoft Research Cambridge, UK
Proving protocols safe from guessing

Catherine Meadows, Naval Research Laboratory, USA
Identifying potential type confusion in authenticated messages

Graham Steel, Alan Bundy, and Ewen Denney; U Edinburgh, UK
Finding counterexamples to inductive conjectures and discovering security protocol attacks

Alessandro Armando, U Genova, Italy; Maria Paola Bonacina, U Iowa, USA; Silvio Ranise, LORIA Nancy, France; Michaël Rusinowitch, LORIA Nancy, France; and Aditya Kumar Sehgal, U Iowa, USA
High-performance deduction for verification: a case study in the theory of arrays

Bernhard Beckert, Uwe Keller, and Peter H. Schmitt; Karlsruhe U, Germany
Translating the object constraint language into first-order predicate logic

Christoph Benzmüller, Saarland U, Germany; Corrado Giromini, Saarland U, Germany; Andreas Nonnengart, DFKI Saarbrücken, Germany; and Jürgen Zimmer, Saarland U, Germany
Reasoning services in MathWeb-SB for symbolic verification of hybrid systems

Amy L. Herzog and Joshua Guttman, MITRE, USA
Eager formal methods for security management

Daniel Kröning, Carnegie Mellon U, USA
Application specific higher order logic theorem proving

Vincent Vanackère, Provence U, Marseille, France
The TRUST protocol analyser, automatic and efficient verification of cryptographic protocols