qest logo
Conference program
Day 1: September 5

9:30 General Opening of QONFEST

10:00-11:00 Invited Talk by Hongseok Yang

11:00-11:30 Coffee/Tea

11:30-13:00 Session 1: Probabilistic modelling

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

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

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


14:30-16:00 Session 2: Special session on Smart Energy and the Cloud

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

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

Boudewijn Haverkort and Marijn Jongerden Battery Aging, Battery Charging and the Kinetic Battery Model

16:00-16:30 Coffee/Tea

16:30-18:30 Session 3: Petri nets and performance evaluation

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

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

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

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

19:00 Welcome reception

Day 2: September 6

9:00-11:00 Session 4 Parametric verification

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

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

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

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

11:00-11:30 Coffee/Tea

11:30-13:00 Session 5: Special session on Machine Learning and Verification

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

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

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


14:00-15:00 Demonstrations of tools

15:00-16:00 Invited Talk by Romualdo Pastor-Satorras

16:00-16:30 Coffee/Tea

16:30-18:00 Panel on Formal methods meets learning

19:30 Banquet

Day 3: September 7

10:00-11:00 Invited Talk by Morten Bisgaard

11:00-11:30 Coffee/Tea

11:30-13:00 Student session

Riccardo Pinciroli, Marco Gribaudo and Giuseppe Serazzi Improving energy efficiency of battery operated pool depletion systems

Sascha Lehmann, Sven-Thomas Antoni, Alexander Schlaefer and Sibylle Schupp Detection of Head Motion Artifacts based on a Statistical Online Model-Checking Approach

Zhihao Shang, Han Wu and Katinka Wolter OpenFlow Controller Scheduling Policy for Mice and Elephant Flow


14:30-16:00 Session 6: Statistical model checking

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

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

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

16:00-16:30 Coffee/Tea

16:30-18:00 Session 7: Tools 

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

Armin Zimmermann Modelling and Performance Evaluation With TimeNET 4.4

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

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