A Logical Account of NGSCB.

Martín Abadi, Ted Wobber

 1-12

Composing Event Constraints in State-Based Specification.

Tommaso Bolognesi

 13-32

Formal Description Techniques and Software Engineering: Some Reflections after 2 Decades of Research.

Juan Quemada

 33-42

Parameterized Models for Distributed Java Objects.

Tomás Barros, Rabéa Boulifa, Eric Madelaine

 43-60

Towards the Harmonisation of UML and SDL.

Rüdiger Grammes, Reinhard Gotzhein

 61-78

Localizing Program Errors for Cimple Debugging.

Samik Basu, Diptikalyan Saha, Scott A. Smolka

 79-96

Formal Verification of a Practical Lock-Free Queue Algorithm.

Simon Doherty, Lindsay Groves, Victor Luchangco, Mark Moir

 97-114

Formal Verification of Web Applications Modeled by Communicating Automata.

May Haydar, Alexandre Petrenko, Houari A. Sahraoui

 115-132

Towards Design Recovery from Observations.

Hasan Ural, Hüsnü Yenigün

 133-149

Network Protocol System Passive Testing for Fault Management: A Backward Checking Approach.

Baptiste Alcalde, Ana R. Cavalli, Dongluo Chen, Davy Khuu, David Lee

 150-166

Connectivity Testing Through Model-Checking.

Jens Chr. Godskesen, Brian Nielsen, Arne Skou

 167-184

Fault Propagation by Equation Solving.

Khaled El-Fakih, Nina Yevtushenko

 185-198

Automatic Generation of Run-Time Test Oracles for Distributed Real-Time Systems.

Xin Wang, Ji Wang, Zhi-Chang Qi

 199-212

Formal Composition of Distributed Scenarios.

Aziz Salah, Rabeb Mizouni, Rachida Dssouli, Benoit Parreaux

 213-228

Conditions for Resolving Observability Problems in Distributed Testing.

Jessica Chen, Robert M. Hierons, Hasan Ural

 229-242

Integrating Formal Verification with Mur ? of Distributed Cache Coherence Protocols in FAME Multiprocessor System Design.

Ghassan Chehaibar

 243-258

Witness and Counterexample Automata for ACTL.

Robert Meolic, Alessandro Fantechi, Stefania Gnesi

 259-275

A Symbolic Symbolic State Space Representation.

Yann Thierry-Mieg, Jean-Michel Ilié, Denis Poitrenaud

 276-291

Introducing the Iteration in sPBC.

Hermenegilda Macià, Valentín Valero Ruiz, Diego Cazorla, Fernando Cuartero

 292-309

Petri Net Semantics of the Finite pi-Calculus.

Raymond R. Devillers, Hanna Klaudel, Maciej Koutny

 309-325

Symbolic Diagnosis of Partially Observable Concurrent Systems.

Thomas Chatain, Claude Jard

 326-342

Automatized Verification of Ad Hoc Routing Protocols.

Oskar Wibling, Joachim Parrow, Arnold Neville Pears

 343-358

A Temporal Logic Based Framework for Intrusion Detection.

Prasad Naldurg, Koushik Sen, Prasanna Thati

 359-376