Chen Li, Taghreed Altamimi, Mana Hassanzadeh Zargari, Giuliano Casale and Dorina Petriu. Tulsa: A Tool for Transforming UML to Layered Queueing Networks for Performance Analysis of Data Intensive Applications.

Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt and Michael Fisher. Investigating Parametric Influence on Discrete Synchronisation Protocols using Quantitative Model Checking.

Cyrille Jegourel, Jun Sun and Jin Song Dong. Sequential Schemes for Estimation of Properties in Statistical Model Checking.

Carmen Cheh, Binbin Chen, William G. Temple and William H. Sanders. Data-Driven Model-Based Detection of Malicious Insiders via Physical Access Logs.

Ludovica Luisa Vissat, Michele Loreti, Laura Nenzi, Jane Hillston and Glenn Marion. Three-Valued Spatio-Temporal Logic: a further analysis on spatio-temporal properties of stochastic systems.

Armin Zimmermann. Modelling and Performance Evaluation With TimeNET 4.4.

Armin Zimmermann, Thomas Hotz and Andres Canabal Lavista. A Hybrid Multi-Trajectory Simulation Algorithm for the Performance Evaluation of Stochastic Petri Nets.

Loic Helouet and Hervé Marchand. On the cost of diagnosis with disambiguation.

Radu Calinescu, Milan Ceska, Simos Gerasimou, Marta Kwiatkowska and Nicola Paoletti. RODES: A Robust-Design Synthesis Tool for Probabilistic Systems.

Elvio Amparore and Susanna Donatelli. alphaFactory: a tool for generating the alpha factors of general distributions.

Anicet Bart, Benoit Delahaye, Didier Lime, Eric Monfroy and Charlotte Truchet. Reachability in Parametric Interval Markov Chains using Constraints.

Michalis Michaelides, Jane Hillston and Guido Sanguinetti. Statistical abstraction for multi-scale spatio-temporal systems.

Youngmin Kwon, Eunhee Kim, Seonghwan Jeong and Arthur Lee. Quantitative Model Checking for a Smart Grid Pricing.

Christel Baier, Clemens Dubslaff, Lubos Korenciak, Antonin Kucera and Vojtech Rehak. Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms.

Andrea Peruffo and Alessandro Abate. An Aggregated Markov Model of an Heterogeneous Population of Photovoltaic Panels.

Elizabeth Polgreen, Viraj Wijesuriya, Sofie Haesaert and Alessandro Abate. Automated experiment design for efficient verification of parametric Markov decision processes.

Marco Biagi, Laura Carnevali, Marco Paolieri, Tommaso Papini and Enrico Vicario. Exploiting non-deterministic analysis in the integration of transient solution techniques for Markov Regenerative Processes.

Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, Morteza Lahijanian and Andrea Turrini. Multi-objective Robust Strategy Synthesis for Interval MDPs.

Marco Baldi, Ezio Bartocci, Franco Chiaraluce, Alessandro Cucchiarelli, Linda Senigagliesi, Luca Spalazzi and Francesco Spegni. A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage.

Pushpak Jagtap and Majid Zamani. QUEST: A Tool for State-Space Quantization-Free Synthesis of Symbolic Controllers.

Vijay Bhattiprolu, Spencer Gordon and Mahesh Viswanathan. Parikh's Theorem for Weighted and Probabilistic Context Free Grammars.

Paul Ezhilchelvan and Isi Mitrani. Multi-class resource sharing with batch arrivals and complete blocking.

Boudewijn Haverkort and Marijn Jongerden. Battery Aging, Battery Charging and the Kinetic Battery Model: A First Exploration.

Sadegh Soudjani, Rupak Majumdar and Tigran Nagapetyan. Multilevel Monte Carlo Method for Statistical Model Checking of Hybrid Systems.