Front matter
1-16
Encoding PAMR into (Timed) EFSMs
Manuel Núñez and Ismael Rodríguez
17-33
Submodule Construction for Specifications with Input Assumptions and Output Guarantees
Gregor v. Bochmann
34-49
Congruent Weak Conformance, a Partial Order among Processes
Ronald W. Brower and Kenneth S. Stevens
50-64
Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures
Farn Wang and Karsten Schmidt
65-80
A Nested Depth First Search Algorithm for Model Checking with Symmetry Reduction
Dragan Bošnački
81-96
Protocol Techniques for Testing Radiotherapy Accelerators
Kenneth J. Turner and Qian Bing
97-113
System Test Synthesis from UML Models of Distributed Software
Simon Pickin, Claude Jard, Yves Le Traon, Thierry Jéron and Jézéquel Jean-Marc, et al.
114-129
Formal Test Purposes and the Validity of Test Cases
Peter H. Deussen and Stephan Tobies
130-145
Use of Logic to Describe Enhanced Communications Services
Stephan Reiff-Marganiec and Kenneth J. Turner
146-161
A Formal Venture into Reliable Multicast Territory
Carolos Livadas and Nancy A. Lynch
162-177
Modelling SIP Services Using Cress
Kenneth J. Turner
178-193
Verifying Reliable Data Transmission over UMTS Radio Interface with High Level Petri Nets
Teemu Tynjälä, Sari Leppänen and Vesa Luukkala
210-225
Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning
Alessandro Armando and Luca Compagna
226-242
Visual Specifications for Modular Reasoning about Asynchronous Systems
Nina Amla, E. Allen Emerson, Kedar S. Namjoshi and Richard J. Trefler
243-259
Bounded Model Checking for Timed Systems
G. Audemard, A. Cimatti, A. Kornilowicz and R. Sebastiani
260-275
C Wolf - A Toolset for Extracting Models from C Programs
Daniel C. Du Varney and S. Purushothaman Iyer
276-291
NTIF: A General Symbolic Model for Communicating Sequential Processes with Data
Hubert Garavel and Frédéric Lang
292-307
Building Tools for LOTOS Symbolic Semantics in Maude
Alberto Verdejo
308-326
From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata
Dimitra Giannakopoulou and Flavio Lerda
327-343
A Compositional Sweep-Line State Space Exploration Method
Lars Michael Kristensen and Thomas Mailund
344-359
On Combining the Persistent Sets Method with the Covering Steps Graph Method
Pierre-Olivier Ribet, Fran çois and Bernard Berthomieu
360-363
Innovative Verification Techniques Used in the Implementation of a Third-Generation 1.1GHz 64b Microprocessor
Victor Melamed, Harry Stuimer, David Wilkins, Lawrence Chang and Kevin Normoyle, et al.
364-368
Mechanical Translation of I/O Automaton Specifications into First-Order Logic
Andrej Bogdanov, Stephen J. Garland and Nancy A. Lynch
369
Verification of Event-Based Synchronization of SpecC Description Using Difference Decision Diagrams
Thanyapat Sakunkonchak and Masahiro Fujita
370
A Distributed Partial Order Reduction Algorithm
Robert Palmer and Ganesh Gopalakrishnan
Back matter