Invited Papers.- Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems.- Satisfiability Checking: Theory and Applications.- Concurrency and Non-Interference.- Automatic Derivation of Platform Noninterference Properties.- Linearizability and Causality.- Refinement-based verification of Communicating Unstructured Code.- Guided Dynamic Symbolic Execution Using Subgraph Control-Flow Information (short paper).-Program Analysis.- Correlating Structured Inputs and Outputs in Functional Specifications.- Combining Predicate Abstraction with Fixpoint Approximations.- Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis.- Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block Diagrams.- Model Checking.- Program Generation using Simulated Annealing and Model Checking.- LTL Parameter Synthesis of Parametric Timed Automata.- Model checking simulation rules for linearizability.- LTL Model Checking under Fairness in ProB (short paper).- Verification.- Counterexamples from Proof Failures in SPARK.- Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution.- SMT-based automatic proof of ASM model refinement.- Coq Implementation of OO Verification Framework VeriJ (short paper).- Towards a Proof Framework for Information Systems with Weak Consistency (short paper).- Interaction and Adaptation.- A Cognitive Framework based on Rewriting Logic for the Analysis of Interactive Systems.- Incentive Stackelberg Mean-payoff Games.- Stability-based Adaptation of Asynchronously Communicating Software.- Compliance Checking in the Open Payments Ecosystem (short paper).- Development Methods.- CoCoSpec: A mode aware contract language.- Modularizing Crosscutting Concerns in Component-Based Systems.- Tightening a Contract Refinement.- BMotionWeb: A Tool for Rapid Creation of Formal Prototypes.
