Invited Papers.- Beyond Nash Equilibrium: Solution Concepts for the 21st Century.- Service Choreography and Orchestration with Conversations.- Knowledge and Information in Probabilistic Systems.- Taming Concurrency: A Program Verification Perspective.- Contributed Papers.- A Model of Dynamic Separation for Transactional Memory.- Completeness and Nondeterminism in Model Checking Transactional Memories.- Semantics of Deterministic Shared-Memory Systems.- A Scalable and Oblivious Atomicity Assertion.- R-Automata.- Distributed Timed Automata with Independently Evolving Clocks.- A Context-Free Process as a Pushdown Automaton.- Modeling Computational Security in Long-Lived Systems.- Contract-Directed Synthesis of Simple Orchestrators.- Environment Assumptions for Synthesis.- Smyle: A Tool for Synthesizing Distributed Models from Scenarios by Learning.- SYCRAFT: A Tool for Synthesizing Distributed Fault-Tolerant Programs.- Subsequence Invariants.- Invariants for Parameterised Boolean Equation Systems.- Unfolding-Based Diagnosis of Systems with an Evolving Topology.- On the Construction of Sorted Reactive Systems.- Dynamic Partial Order Reduction Using Probe Sets.- A Space-Efficient Probabilistic Simulation Algorithm.- Least Upper Bounds for Probability Measures and Their Applications to Abstractions.- Abstraction for Stochastic Systems by Erlang’s Method of Stages.- On the Minimisation of Acyclic Models.- Quasi-Static Scheduling of Communicating Tasks.- Strategy Construction for Parity Games with Imperfect Information.- Mixing Lossy and Perfect Fifo Channels.- On the Reachability Analysis of Acyclic Networks of Pushdown Systems.- Spatial and Behavioral Types in the Pi-Calculus.- A Spatial Equational Logic for the Applied ?-Calculus.- Structured Interactional Exceptions inSession Types.- Global Progress in Dynamically Interleaved Multiparty Sessions.- Normed BPA vs. Normed BPP Revisited.- A Rule Format for Associativity.- Deriving Structural Labelled Transitions for Mobile Ambients.- Termination Problems in Chemical Kinetics.- Towards a Unified Approach to Encodability and Separation Results for Process Calculi.- A Notion of Glue Expressiveness for Component-Based Systems.