InhaltsangabeInvited Talks.- Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode.- Perspectives in Certificate Translation.- Uniform Labeled Transition Systems for Nondeterministic, Probabilistic, and Stochastic Processes.- Toward a Game-Theoretic Model of Grid Systems.- Functions as Processes: Termination and the -Calculus.- Predicate Encryption for Secure Remote Storage.- Trust in Crowds: Probabilistic Behaviour in Anonymity Protocols.- Types and Processes.- Expressiveness of Generic Process Shape Types.- A Java Inspired Semantics for Transactions in SOC.- Responsive Choice in Mobile Processes.- A Model of Evolvable Components.- Games and Concurrent Systems.- The Impact of Altruism on the Efficiency of Atomic Congestion Games.- Stressed Web Environments as Strategic Games: Risk Profiles and Weltanschauung.- An Algebra of Hierarchical Graphs.- Property-Preserving Refinement of Concurrent Systems.- Certification of Correctness.- Certificate Translation for the Verification of Concurrent Programs.- Certified Result Checking for Polyhedral Analysis of Bytecode Programs.- Tools and Languages.- A Novel Resource-Driven Job Allocation Scheme for Desktop Grid Environments.- A Framework for Rule-Based Dynamic Adaptation.- CarPal: Interconnecting Overlay Networks for a Community-Driven Shared Mobility.- Refactoring Long Running Transactions: A Case Study.- Probabilistic Aspects.- Approximate Model Checking of Stochastic COWS.- Probabilistic Aspects: Checking Security in an Imperfect World.- A Tool for Checking Probabilistic Properties of COWS Services.