[Front cover]

Title Page i (PDF)

pp. i

Title Page iii (PDF)

pp. iii

[Copyright notice] (PDF)

pp. iv

Table of contents (PDF)

pp. v-vii

Message from the General Chair (PDF)

pp. viii

Message from the Program Committee Co-chairs (PDF)

pp. ix-x

Organizing Committee (PDF)

pp. xi

Technical Program Committee (PDF)

pp. xii

Reviewers (PDF)

pp. xiii

Hybrid Limits of Continuous Time Markov Chains (Abstract)

Luca Bortolussi

pp. 3-12

PDF

Fluid Limits Applied to Peer to Peer Network Analysis (Abstract)

pp. 13-20

PDF

Fluid Analysis of Queueing in Two-Stage Random Environments (Abstract)

Giuliano Casale

Mirco Tribastone

pp. 21-30

PDF

Temperature-aware Real-Time Scheduling - Extended Abstract (Abstract)

Lothar Thiele

pp. 33-34

PDF

A Tool for Scalable Profiling and Tracing of Java and Native Code Interactions (Abstract)

pp. 37-46

PDF

A Hybrid Approach for Large Cache Performance Studies (Abstract)

pp. 47-56

PDF

Sadegh Esmaeil Zadeh Soudjani

Adaptive Gridding for Abstraction and Verification of Stochastic Hybrid Systems (Abstract)

Alessandro Abate

pp. 59-68

PDF

Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems (Abstract)

pp. 69-78

PDF

Discrete-Time Verification and Control for Probabilistic Rectangular Hybrid Automata (Abstract)

Jeremy Sproston

pp. 79-88

PDF

MARCIE - Model Checking and Reachability Analysis Done EffiCIEntly (Abstract)

pp. 91-100

PDF

Probe Automata for Passage Time Specification (Abstract)

Elvio Gilberto Amparore

Marco Beccuti

Susanna Donatelli

Giuliana Franceschinis

pp. 101-110

PDF

Learning Probabilistic Automata for Model Checking (Abstract)

Hua Mao

pp. 111-120

PDF

Model Checking MDPs with a Unique Compact Invariant Set of Distributions (Abstract)

Rohit Chadha

Vijay Anand Korthikanti

pp. 121-130

PDF

Probabilistic Model Checking of Non-Markovian Models with Concurrent Generally Distributed Timers (Abstract)

pp. 131-140

PDF

COSMOS: A Statistical Model Checker for the Hybrid Automata Stochastic Logic (Abstract)

pp. 143-144

PDF

A Tool: Quantitative Analyser for Programs (Abstract)

Chunyan Mu

David Clark

pp. 145-146

PDF

GPA - A Tool for Fluid Scalability Analysis of Massively Parallel Systems (Abstract)

pp. 147-148

PDF

SCOOP: A Tool for SymboliC Optimisations of Probabilistic Processes (Abstract)

Mark Timmer

pp. 149-150

PDF

APAC: A Tool for Reasoning about Abstract Probabilistic Automata (Abstract)

pp. 151-152

PDF

Sirio: A Framework for Simulation and Symbolic State Space Analysis of non-Markovian Models (Abstract)

pp. 153-154

PDF

SPORTSBET: A Tool for the Quantitative Evaluation and Execution of Betting Exchange Trading Strategies (Abstract)

Polyvios Tsirimpas

William J. Knottenbelt

pp. 155-156

PDF

Quantifying Information Flow Using Min-Entropy (Abstract)

Geoffrey Smith

pp. 159-167

PDF

Controlling Modelling Artifacts (Abstract)

pp. 171-180

PDF

Forecasting Run-Times of Secure Two-Party Computation (Abstract)

Axel Schröepfer

Florian Kerschbaum

pp. 181-190

PDF

Model-based Security Metrics Using ADversary VIew Security Evaluation (ADVISE) (Abstract)

pp. 191-200

PDF

Partial Order Reduction for Model Checking Markov Decision Processes under Unconditional Fairness (Abstract)

pp. 203-212

PDF

Composition and Equivalence of Markovian and Non-Markovian Models (Abstract)

Peter Buchholz

Miklós Telek

pp. 213-222

PDF

Compositional Abstractions for Long-Run Properties of Stochastic Systems (Abstract)

Michael J.A. Smith

pp. 223-232

PDF

The Multiple-Asymmetric-Utility System Model: A Framework for Modeling Cyber-Human Systems (Abstract)

Douglas Eskins

William H. Sanders

pp. 233-242

PDF

A Modeling Framework for Gossip-based Information Spread (Abstract)

pp. 245-254

PDF

Quantitative Evaluation of BFT Protocols (Abstract)

pp. 255-264

PDF

Performance Comparison of Aggressive Push and Traditional Pull Strategies in Large Distributed Systems (Abstract)

Benny Van Houdt

pp. 265-274

PDF

Author Index (PDF)

pp. 275-276

[Roster page] (PDF)

pp. 278