CONCUR 2004 – Concurrency Theory: 15th International Conference, London, UK, August 31 – September 3, 2004. Proceedings

Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, Yichen Xie (auth.), Philippa Gardner, Nobuko Yoshida (eds.)9783540229407, 354022940X, 9783540286448

This book constitutes the refereed proceedings of the 15th International Conference on Concurrency Theory, CONCUR 2004, held in London, UK in August/September 2004.

The 29 revised full papers presented together with 4 invited papers were carefully reviewed and selected from 134 submissions. Among the topics covered are concurrency related aspects of models of computation, semantic domains, process algebras, Petri nets, event structures, real-time systems, hybrid systems, decidability, model checking, verification techniques, refinement, term and graph rewriting, distributed programming, constraint logic programming, object-oriented programming, typing systems and algorithms, case studies, tools, and environments for programming and verification.

---

Table of contents :
Front Matter….Pages –
Zing: Exploiting Program Structure for Model Checking Concurrent Software….Pages 1-15
A Semantics for Concurrent Separation Logic….Pages 16-34
A Survey of Regular Model Checking….Pages 35-48
Resources, Concurrency and Local Reasoning….Pages 49-67
Resource Control for Synchronous Cooperative Threads….Pages 68-82
Verifying Finite-State Graph Grammars: An Unfolding-Based Approach….Pages 83-98
The Pros and Cons of Netcharts….Pages 99-114
Basic Theory of Reduction Congruence forTwo Timed Asynchronous π -Calculi….Pages 115-130
Characterizing EF and EX Tree Logics….Pages 131-145
Message-Passing Automata Are Expressively Equivalent to EMSO Logic….Pages 146-160
Symbolic Bisimulation in the Spi Calculus….Pages 161-176
A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps….Pages 177-192
Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems….Pages 193-208
μ ABC: A Minimal Aspect Calculus….Pages 209-224
Type Based Discretionary Access Control….Pages 225-239
Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency….Pages 240-257
Modular Construction of Modal Logics….Pages 258-275
Verification by Network Decomposition….Pages 276-291
Reversible Communicating Systems….Pages 292-307
Parameterised Boolean Equation Systems….Pages 308-324
An Extensional Spatial Logic for Mobile Processes….Pages 325-339
Timed vs. Time-Triggered Automata….Pages 340-354
Extended Process Rewrite Systems: Expressiveness and Reachability….Pages 355-370
A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications….Pages 371-386
Model Checking Timed Automata with One or Two Clocks….Pages 387-401
On Flatness for 2-Dimensional Vector Addition Systems with States….Pages 402-416
Compiling Pattern Matching in Join-Patterns….Pages 417-431
Model Checking Restricted Sets of Timed Paths….Pages 432-447
Asynchronous Games 2: The True Concurrency of Innocence….Pages 448-465
Open Maps, Alternating Simulations and Control Synthesis….Pages 466-480
Probabilistic Event Structures and Domains….Pages 481-496
Session Types for Functional Multithreading….Pages 497-511
A Higher Order Modal Fixed Point Logic….Pages 512-528
Back Matter….Pages –