Keynote Presentations.- Quantitative Evaluation of Service Dependability in Shared Execution Environments.- Multi-agent Networked Systems with Adversarial Elements.- Kronecker and Product Form Methods.- A Structured Solution Approach for Markov Regenerative Processes.- Low-Rank Tensor Methods for Communicating Markov Processes.- Hybrid Systems.- A Statistical Approach for Computing Reachability of Non-linear and Stochastic Dynamical Systems.- Formal Synthesis and Validation of Inhomogeneous Thermostatically Controlled Loads.- Finite Abstractions of Stochastic Max-Plus-Linear Systems.- Mean Field/Population Analysis.- Mean Field for Performance Models with Generally-Distributed Timed Transitions.- Mean-Field Approximation and Quasi-Equilibrium Reduction of Markov Population Models.- On Performance of Gossip Communication in a Crowd-Sensing Scenario.- Models and Tools.- Probabilistic Model Checking of DTMC Models of User Activity Patterns.- Performance Comparison of IEEE 802.11 DCF and EDCA for Beaconing in Vehicular Networks.- A New Great SPN GUI for GSPN Editing and CSLTA Model Checking.- The Octave Queueing.- Package.- Simulation.- A Perfect Sampling Algorithm of Random Walks with Forbidden Arcs.- Modelling Replication in No SQL Datastores.- Queueing, Debugging and Tools.- On Queues with General Service Demands and Constant Service Capacity.- Simulation Debugging and Visualization in the Mobius Modeling Framework.- Scalar: A Distributed Scalability Analysis Framework.- Non-intrusive Scalable Memory Access Tracer.- Process Algebra and Equivalences.- Probabilistic Programming Process Algebra.- PALOMA: A Process Algebra for Located Markovian Agents.- On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems.- Automata and Markov Process Theory.- Continuity Properties of Distances for Markov Processes.- Deciding the Value 1 Problem for Reachability in 1-Clock Decision Stochastic Timed Automata.- Decidable Problems for Unary PFAs.- Applications, Theory and Tools.- A Scalable Approach to the Assessment of Storm Impact in Distributed Automation Power Grids.- Compositionality Results for Quantitative Information Flow.- CyberSAGE: A Tool for Automatic Security Assessment of Cyber-Physical Systems.- Probabilistic Model Checking.- Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains.- Accelerating Parametric Probabilistic Verification.