Volume 128, Number 1, May 2005

Proceedings of the Workshop on Structural Operational Semantics (SOS 2004)

• 
  Luca Aceto, Wan Fokkink, Irek Ulidowski: Preface. 1-
• 
  Bartek Klin: From Bialgebraic Semantics to Congruence Formats. 3-37
• 
  Marija Kulas: Toward the Concept of Backtracking Computation. 39-59
• 
  Ralf Lämmel: Evolution Scenarios for Rule-Based Implementations of Language-Based Functionality. 61-79
• 
  Matthias Mann: Congruence of Bisimulation in a Non-Deterministic Call-By-Need Lambda Calculus. 81-101
• 
  Olivier Tardieu: A Deterministic Logical Semantics for Esterel. 103-122

Volume 128, Number 2, April 2005

Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS 2004)

• 
  Jos C. M. Baeten, Flavio Corradini: Preface. 1-3
• 
  Rob J. van Glabbeek: On the Expressiveness of Higher Dimensional Automata: (Extended Abstract). 5-34
• 
  Flavio Corradini, Maria Rita Di Berardini, Walter Vogler: Fairness of Components in System Computations. 35-52
• 
  Suzana Andova, Tim A. C. Willemse: Equivalences for Silent Transitions in Probabilistic Systems: (Extended Abstract). 53-66
• 
  Emmanuel Beffara, François Maurel: Concurrent Nets: A Study of Prefixing in Process Calculi. 67-86
• 
  Alain Finkel, Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin: On the omega-language Expressive Power of Extended Petri Nets. 87-101
• 
  Harald Fecher, Martin Steffen: Characteristic mu-Calculus Formulas for Underspecified Transition Systems. 103-116
• 
  Rocco De Nicola, Daniele Gorla, Rosario Pugliese: On the Expressive Power of Klaim-based Calculi. 117-130
• 
  Mikkel Bundgaard, Thomas T. Hildebrandt, Jens Chr. Godskesen: A CPS Encoding of Name-Passing in Higher-Order Mobile Embedded Resources. 131-150
• 
  Reynald Affeldt, Naoki Kobayashi: Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes. 151-168
• 
  Xudong Guan: Name-Passing in an Ambient-Like Calculus and Its Proof Using Spatial Logic. 169-183
• 
  Iain Phillips, Maria Grazia Vigliotti: Leader Election in Rings of Ambient Processes. 185-199

Volume 128, Number 3, April 2005

Proceedings of the 3rd International Workshop on Parallel and Distributed Methods in Verification (PDMC 2004)

• 
  Lubos Brim, Martin Leucker: Preface. 1-2
• 
  Víctor A. Braberman, Alfredo Olivero, Fernando Schapachnik: On-the-fly Workload Prediction and Redistribution in the Distributed Timed Model Checker Zeus. 3-18
• 
  Rahul Kumar, Eric G. Mercer: Load Balancing Parallel Explicit State Model Checking. 19-34
• 
  Simona Orzan, Jaco van de Pol, Miguel Valero Espada: A State Space Distribution Policy Based on Abstract Interpretation. 35-45
• 
  Christophe Joubert, Radu Mateescu: Distributed On-the-Fly Equivalence Checking. 47-62
• 
  Lubos Brim, Ivana Cerná, Pavel Moravec, Jirí Simsa: Distributed Partial Order Reduction of State Spaces. 63-74
• 
  Yulik Feldman, Nachum Dershowitz, Ziyad Hanna: Parallel Multithreaded Satisfiability Solver: Design and Implementation. 75-90
• 
  Fredrik Holmén, Martin Leucker, Marcus Lindström: UppDMC: A Distributed Model Checker for Fragments of the mu-Calculus. 91-105
• 
  Cornelia P. Inggs, Howard Barringer: CTL^* Model Checking on a Shared-Memory Architecture. 107-123
• 
  Martin Lange, Hans-Wolfgang Loidl: Parallel and Symbolic Model Checking for Fixpoint Logic with Chop. 125-138

Volume 128, Number 4, April 2005

Proceedings of the First International Workshop on Practical Applications of Stochastic Modelling (PASM 2004)

• 
  Jeremy T. Bradley, William J. Knottenbelt: Preface. 1-2
• 
  Nil Geisweiller, Jeremie Bonte: Performance Evaluation of a Real-time Simulation Architecture using Probabilistic Model Checking. 3-24
• 
  Gábor Horváth, Miklós Telek: Analysis of a BMAP/D/1-Timer Multiplexer. 25-44
• 
  Nigel Thomas: Performability of a Secure Electronic Voting Algorithm. 45-58
• 
  Carlo Bellettini, Lorenzo Capra, Mattia Monga: Quantitative Assessment of a Peer-to-peer Cooperative Infrastructure Using Stochastic Well-Formed Nets. 59-77
• 
  Rossano Gaeta, Marco Gribaudo, Daniele Manini, Matteo Sereno: Fluid Stochastic Petri Nets for Computing Transfer Time Distributions in Peer-to-Peer File Sharing Applications. 79-99
• 
  Lucas Baldo, Leonardo Brenner, Luiz Gustavo Fernandes, Paulo Fernandes, Afonso Sales: Performance Models For Master/Slave Parallel Programs. 101-121
• 
  Mikael Buchholtz, Stephen T. Gilmore, Jane Hillston, Flemming Nielson: Securing Statically-verified Communications Protocols Against Timing Attacks. 123-143
• 
  Peter G. Harrison, Soraya Zertal: Calibration of a Queueing Model of RAID Systems. 145-164

Volume 128, Number 5, May 2005

Proceedings of the 2nd International Workshop on Security Issues in Coordination Models, Languages, and Systems (SecCo 2004)

• 
  Riccardo Focardi, Gianluigi Zavattaro: Preface. 1-2
• 
  Lorenzo Bettini: Data Privacy in Tuple Space Based Mobile Agent Systems. 3-16
• 
  Chiara Braghin, Agostino Cortesi: Flow-sensitive Leakage Analysis in Mobile Ambients. 17-25
• 
  Alessandra Di Pierro, Chris Hankin, Herbert Wiklicky: Continuous-Time Probabilistic KLAIM. 27-38
• 
  Mario Bravetti, Roberto Gorrieri, Roberto Lucchi, Gianluigi Zavattaro: On the Expressiveness of Probabilistic and Prioritized Data-retrieval in Linda. 39-53
• 
  Matteo Maffei: Tags for Multi-Protocol Authentication. 55-63
• 
  Andrea Omicini, Alessandro Ricci, Mirko Viroli: RBAC for Organisation and Security in an Agent Coordination Infrastructure. 65-85
• 
  Steve Kremer, Mark Ryan: Analysing the Vulnerability of Protocols to Produce Known-pair and Chosen-text Attacks. 87-104
• 
  Maurice H. ter Beek, Gabriele Lenzini, Marinella Petrocchi: Team Automata for Security: - A Survey -. 105-119

Volume 128, Number 6, May 2005

Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems (AVoCS 2004)

• 
  Michael Huth: Preface. 1-2
• 
  Armelle Merlin, Gaétan Hains: A Generic Cost Model for Concurrent and Data-parallel Meta-computing. 3-19
• 
  Nils Klarlund, Richard J. Trefler: Regularity Results for FIFO Channels. 21-36
• 
  Lee Momtahan: Towards a Small Model Theorem for Data Independent Systems in Alloy. 37-52
• 
  Wan Fokkink, Jun Pang: Simplifying Itai-Rodeh Leader Election for Anonymous Rings. 53-68
• 
  Jean-François Raskin, Mathias Samuelides, Laurent Van Begin: Games for Counting Abstractions. 69-85
• 
  Christophe Darlot, Alain Finkel, Laurent Van Begin: About Fast and TReX Accelerations. 87-103
• 
  Aleksandar Dimovski, Ranko Lazic: Software Model Checking Based on Game Semantics and CSP. 105-125
• 
  Philippa J. Hopcroft, Guy H. Broadfoot: Combining the Box Structure Development Method and CSP for Software Development. 127-144
• 
  Franck Cassez, Olivier H. Roux: Structural Translation from Time Petri Nets to Timed Automata. 145-160
• 
  Alastair F. Donaldson, Alice Miller, Muffy Calder: Finding Symmetry in Models of Concurrent Systems by Static Channel Diagram Analysis. 161-177
• 
  Radu Siminiceanu, Gianfranco Ciardo: Formal Verification of the NASA Runway Safety Monitor. 179-194
• 
  Marie Duflot, Laurent Fribourg, Thomas Hérault, Richard Lassaigne, Frédéric Magniette, Stéphane Messika, Sylvain Peyronnet, Claudine Picaronny: Probabilistic Model Checking of the CSMA/CD Protocol Using PRISM and APMC. 195-214
• 
  Harald Fecher: Truly Concurrent Logic via In-Between Specification. 215-230
• 
  Xu Wang, Marta Z. Kwiatkowska, Georgios K. Theodoropoulos, Qianyi Zhang: Towards a Unifying CSP approach to Hierarchical Verification of Asynchronous Hardware. 231-246
• 
  Paritosh K. Pandya: Finding Extremal Models of Discrete Duration Calculus formulae using Symbolic Search. 247-262
• 
  Cécile Braunstein, Emmanuelle Encrenaz: CTL-Property Transformations Along an Incremental Design Process. 263-278
• 
  Shobha Vasudevan, E. Allen Emerson, Jacob A. Abraham: Efficient Model Checking of Hardware Using Conditioned Slicing. 279-294
• 
  Marco Gribaudo, András Horváth: Model Checking Functional and Performability Properties of Stochastic Fluid Models. 295-310
• 
  Dimitar P. Guelev, Mark Dermot Ryan, Pierre-Yves Schobbens: Model-checking the Preservation of Temporal Properties upon Feature Integration. 311-324