Regular papers

Thomas Arts, Ericsson, Sweden; Clara Benac Earle, U Kent-Canterbury, UK; and John Derrick, U Kent-Canterbury, UK
Verifying Erlang code: a resource locker case-study

Michael Backes, Saarland U, Germany; Christian Jacobi, Saarland U, Germany; and Birgit Pfitzmann, IBM Zürich, Switzerland
Deriving cryptographically sound implementations using composition and formally verified bisimulation

Sharon Barner, Shoham Ben-David, Anna Gringauze, Baruch Sterin, and Yaron Wolfsthal; IBM Haifa, Israel
An algorithmic approach to design exploration

Juan Bicarregui, Rutherford Appleton Laboratory, UK
Do not read this

Igor B. Bourdonov, Alexander S. Kossatchev, Victor V. Kuliamin, and Alexander K. Petrenko; ISP/RAS Moscow, Russia
UniTesK test suite architecture

Juan C. Burguillo-Rial, Manuel J. Fernández-Iglesias, Francisco J. Gonzáles-Castaño, and Martín Llamas-Nistal; U Vigo, Spain
Heuristic-driven test case selection from formal specifications. A case study

Ludovic Casset, Gemplus Research Laboratory, France
Development of an embedded verifier for Java Card byte code using formal methods

Néstor Cataño and Marieke Huisman, INRIA Sophia-Antipolis, France
Formal specification and static checking of Gemplus' electronic purse using ESC/Java

Ana Cavalcanti, Federal U of Pernambuco, Brazil and David A. Naumann, Stevens Inst. of Techn., USA
Forward simulation for data refinement of classes

María Victoria Cengarle, Techn. U of Munich, Germany and Alexander Knapp, U Munich, Germany
Towards OCL/RT

Jin Song Dong, Jing Sun, and Hai Wang; National U of Singapore
Semantic web for extending and linking formalisms

C. J. Fidge, U Queensland, Australia
Timing analysis of assembler code control-flow paths

Thomas Firley and Ursula Goltz, Techn. U of Braunschweig, Germany
Property dependent abstraction of control structure for software verification

Hubert Garavel, INRIA Rhône-Alpes, France and Holger Hermanns, U Twente, The Netherlands
On combining functional verification and performance evaluation using CADP

Neil Henderson, U Newcastle upon Tyne, UK and Stephen Paynter, MBDA Ltd, UK
The formal classification and verification of Simpson's 4-slot asynchronous communication mechanism

Michael Huber, Siemens Transportation Systems, Switzerland and Steve King, U York, UK
Towards an integrated model checker for railway signalling data

Natalia Ioustinova, CWI Amsterdam, The Netherlands; Natalia Sidorova, Eindhoven U of Techn., The Netherlands; and Martin Steffen, U Kiel, Germany
Closing open SDL-systems for model checking with DTSpin

Niels Jørgensen, U Roskilde, Denmark
Safeness of make-based incremental recompilation

Lars Michael Kristensen, U South Australia, Australia and Thomas Mailund, U Aarhus, Denmark
A generalised sweep-line method for safety properties

Bruno Legeard, U Franche-Comté, France; Fabien Peureux, U Franche-Comté, France; and Mark Utting, U Waikato, New Zealand
Automated boundary testing from Z and B

Darko Marinov and Sarfraz Khurshid, Massachusetts Inst. of Techn., USA
VAlloy - virtual functions meet a relational language

Alexandre Mota, Paulo Borba, and Augusto Sampaio; Federal U of Pernambuco, Brazil
Mechanical abstraction of CSP_Z processes

Claus Pahl, Dublin City U, Ireland
Interference analysis for dependable systems using refinement and abstraction

Gil Ratsaby, Baruch Sterin, and Shmuel Ur; IBM Haifa, Israel
Improvements in coverability analysis

Vlad Rusu, IRISA Rennes, France
Verification using test generation techniques

Augusto Sampaio, Federal U of Pernambuco, Brazil; Jim Woodcock, U Kent-Canterbury, UK; and Ana Cavalcanti, Federal U of Pernambuco, Brazil
Refinement in Circus

Helen Treharne, Royal Holloway, U London, UK
Supplementing a UML development process with B

Takaaki Umedu, Osaka U, Japan; Yoshiki Terashima, Osaka U, Japan; Keiichi Yasumoto, Nara Inst. of Science and Techn., Japan; Akio Nakata, Osaka U, Japan; Teruo Higashino, Osaka U, Japan; and Kenichi Taniguchi, Osaka U, Japan
A language for describing wireless mobile applications with dynamic establishment of multi-way synchronization channels

David von Oheimb and Tobias Nipkow, Techn. U of Munich, Germany
Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited

Michael Whalen, U Minnesota, USA; Johann Schumann, NASA Ames, USA; and Bernd Fischer, NASA Ames, USA
Synthesizing certified code

Luke Wildman, U Queensland, Australia
A formal basis for a program compilation proof tools