Inhaltsverzeichnis
Invited Papers. - Zing: Exploiting Program Structure for Model Checking Concurrent Software. - A Semantics for Concurrent Separation Logic. - A Survey of Regular Model Checking. - Resources, Concurrency and Local Reasoning. - Accepted Papers. - Resource Control for Synchronous Cooperative Threads. - Verifying Finite-State Graph Grammars: An Unfolding-Based Approach. - The Pros and Cons of Netcharts. - Basic Theory of Reduction Congruence forTwo Timed Asynchronous ? -Calculi. - Characterizing EF and EX Tree Logics. - Message-Passing Automata Are Expressively Equivalent to EMSO Logic. - Symbolic Bisimulation in the Spi Calculus. - A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps. - Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems. - ? ABC: A Minimal Aspect Calculus. - Type Based Discretionary Access Control. - Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency. - Modular Construction of Modal Logics. - Verification by Network Decomposition. - Reversible Communicating Systems. - Parameterised Boolean Equation Systems. - An Extensional Spatial Logic for Mobile Processes. - Timed vs. Time-Triggered Automata. - Extended Process Rewrite Systems: Expressiveness and Reachability. - A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications. - Model Checking Timed Automata with One or Two Clocks. - On Flatness for 2-Dimensional Vector Addition Systems with States. - Compiling Pattern Matching in Join-Patterns. - Model Checking Restricted Sets of Timed Paths. - Asynchronous Games 2: The True Concurrency of Innocence. - Open Maps, Alternating Simulations and Control Synthesis. - Probabilistic Event Structures and Domains. - Session Types for Functional Multithreading. - A Higher Order Modal FixedPoint Logic.