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
Parikh's Theorem for Weighted and Probabilistic Context Free Grammars
Exploiting non-deterministic analysis in the integration of transient solution techniques for Markov Regenerative Processes
alphaFactory: a tool for generating the alpha factors of general distributions
Lunch
14:30-16:00 Session 2: Special session on Smart Energy and the Cloud
Quantitative Model Checking for a Smart Grid Pricing
An Aggregated Markov Model of an Heterogeneous Population of Photovoltaic Panels
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
A Hybrid Multi-Trajectory Simulation Algorithm for the Performance Evaluation of Stochastic Petri Nets
A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage
On the cost of diagnosis with disambiguation
Multi-class resource sharing with batch arrivals and complete blocking
19:00 Welcome reception
9:00-11:00 Session 4 Parametric verification
Reachability in Parametric Interval Markov Chains using Constraints
Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms
Multi-objective Robust Strategy Synthesis for Interval MDPs
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
Statistical abstraction for multi-scale spatio-temporal systems
Automated experiment design for efficient verification of parametric Markov decision processes
Data-Driven Model-Based Detection of Malicious Insiders via Physical Access Logs
Lunch
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
10:00-11:00 Invited Talk by Morten Bisgaard
11:00-11:30 Coffee/Tea
11:30-13:00 Student session
Improving energy efficiency of battery operated pool depletion systems
Detection of Head Motion Artifacts based on a Statistical Online Model-Checking Approach
OpenFlow Controller Scheduling Policy for Mice and Elephant Flow
Lunch
14:30-16:00 Session 6: Statistical model checking
Three-Valued Spatio-Temporal Logic: a further analysis on spatio-temporal properties of stochastic systems
Sequential Schemes for Estimation of Properties in Statistical Model Checking
Multilevel Monte Carlo Method for Statistical Model Checking of Hybrid Systems
16:00-16:30 Coffee/Tea
16:30-18:00 Session 7: Tools
Tulsa: A Tool for Transforming UML to Layered Queueing Networks for Performance Analysis of Data Intensive Applications
Modelling and Performance Evaluation With TimeNET 4.4
RODES: A Robust-Design Synthesis Tool for Probabilistic Systems
QUEST: A Tool for State-Space Quantization-Free Synthesis of Symbolic Controllers
Closing