CONCUR 2000 - Concurrency Theory

- Invited Talks
- Combining Theorem Proving and Model Checking through Symbolic Analysis
- Verification Is Experimentation!
- Compositional Performance Analysis Using Probabilistic I/O Automata
- Formal Models for Communication-Based Design
- Invited Tutorials
- Programming Access Control: The Klaim Experience
- Exploiting Hierarchical Structure for Efficient Formal Verification
- From Process Calculi to Process Frameworks
- Verification Using Tabled Logic Programming
- Accepted Papers
- Open Systems in Reactive Environments: Control and Synthesis
- Model Checking with Finite Complete Prefixes Is PSPACE-Complete
- Verifying Quantitative Properties of Continuous Probabilistic Timed Automata
- The Impressive Power of Stopwatches
- Optimizing Büchi Automata
- Generalized Model Checking: Reasoning about Partial State Spaces
- Reachability Analysis for Some Models of Infinite-State Transition Systems
- Process Spaces
- Failure Semantics for the Exchange of Information in Multi-Agent Systems
- Proof-Outlines for Threads in Java
- Deriving Bisimulation Congruences for Reactive Systems
- Bisimilarity Congruences for Open Terms and Term Graphs via Tile Logic
- Process Languages for Rooted Eager Bisimulation
- Action Contraction
- A Theory of Testing for Markovian Processes
- Reasoning about Probabilistic Lossy Channel Systems
- Weak Bisimulation for Probabilistic Systems
- Nondeterminism and Probabilistic Choice: Obeying the Laws
- Secrecy and Group Creation
- On the Reachability Problem in Cryptographic Protocols
- Secure Information Flow for Concurrent Processes
- LP Deadlock Checking Using Partial Order Dependencies
- Pomsets for Local Trace Languages
- Functional Concurrent Semantics for Petri Nets with Read and Inhibitor Arcs
- The Control of Synchronous Systems
- Typing Non-uniform Concurrent Objects
- An Implicitly-Typed Deadlock-Free Process Calculus
- Typed Mobile Objects
- Synthesizing Distributed Finite-State Systems from