Accepted Papers
Regular papers
Tool papers
| Luca Bortolussi | Hybrid Limits of Continuous Time Markov Chains |
| Giuliano Casale and Mirco Tribastone | Fluid Analysis of Queueing in Random Environments |
| Rena Bakhshi, Daniela Gavidia, Wan Fokkink and Maarten Van Steen | A Modeling Framework for Gossip-based Information Spread |
| Henri Hansen, Hongyang Qu and Marta Kwiatkowska | Partial order reduction for Model checking MDPs under unconditional fairness |
| Peter Buchholz and Miklos Telek | Composition and Equivalence of Markovian and Non-Markovian Models |
| Andras Horvath, Marco Paolieri, Lorenzo Ridi and Enrico Vicario | Bounded model checking of generalized semi-Markov processes using stochastic state classes |
| Rohit Chadha, Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha and Youngmin Kwon | Model Checking MDPs With A Unique Invariant Set of Distributions |
| Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate | Adaptive Gridding for Abstraction and Verification of Stochastic Hybrid Systems |
| Ernst Moritz Hahn, Gethin Norman, Dave Parker, Björn Wachter and Lijun Zhang | Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems |
| Jeremy Sproston | Discrete-Time Verification and Control for Probabilistic Rectangular Hybrid Automata |
| Martin Schwarick, Christian Rohr and Monika Heiner | MARCIE - Model checking And Reachability analysis done effiCIEntly |
| Axel Schroepfer and Florian Kerschbaum | Forecasting Run-Times of Secure Two-Party Computation |
| Michael Smith, Flemming Nielson and Hanne Riis Nielson | Controlling Modelling Artifacts |
| Douglas Eskins and William Sanders | The Multiple-Asymmetric-Utility System Model: A Framework for Modeling Cyber-Human Systems |
| Yingke Chen, Hua Mao, Manfred Jaeger, Thomas D. Nielsen, Kim G. Larsen and Brian Nielsen | Learning Probabilistic Automata for Model Checking |
| Michael Smith | Compositional Abstractions for Long-Run Properties of Stochastic Systems |
| Elvio Gilberto Amparore, Marco Beccuti, Susanna Donatelli and Giuliana Franceschinis | Probe Automata for Passage Time Specification |
| David Daly, Parijat Dube, Kaoutar El Maghraoui and Zhang Li | A Hybrid Approach for Large Cache Performance Studies |
| Elizabeth Lemay, Michael D. Ford, Ken Keefe, Carol Muehrcke and William H. Sanders | Model-based Security Metrics using ADversary VIew Security Evaluation (ADVISE) |
| Benny Van Houdt | Performance comparison of aggressive push and traditional pull strategies in large distributed systems |
| Laura Aspirot, Ernesto Mordecki and Gerardo Rubino | Fluid Limits and Mean field Approximations Applied to Peer to Peer Network Analysis |
| Raluca Halalai, Thomas A. Henzinger and Vasu Singh | Quantitative Evaluation of BFT Protocols |
| Parijat Dube, Seetharami Seelam, Yanbin Liu, Megumi Ito, Michel Hack, Liana Fong, Graeme Johnson, Michael Dawson, Li Zhang and Yuqing Gao | A Tool for Scalable Profiling and Tracing of Java and Native Code Interactions |
Tool papers
| Paolo Ballarini, Hilal Djafri, Serge Haddad, Marie Duflot and Nihal Pekergin | COSMOS: a Statistical Model Checker for the Hybrid Automata Stochastic Logic |
| Chunyan Mu and David Clark | A QIF Analyser for Programs in a Simple Language |
| Anton Stefanek, Richard Hayden and Jeremy Bradley | GPA ? a tool for fluid scalability analysis of massively parallel systems |
| Mark Timmer | SCOOP: A Tool for SymboliC Optimisations Of Probabilistic Processes |
| Axel Legay, Mikkel L. Pedersen, Benoit Delahaye, Andrzej Wasowski and Kim. G Larsen | APAC: a tool for reasoning about Abstract Probabilistic Automata |
| Laura Carnevali, Lorenzo Ridi and Enrico Vicario | Sirio: A framework for simulation and symbolic state space analysis of non-Markovian models |
| Polyvios Tsirimpas and William Knottenbelt | SPORTSBET: A Tool for the Quantitative Evaluation and Execution of Betting Exchange Trading Strategies |