Write a Blog >>
ASE 2020
Mon 21 - Fri 25 September 2020 Melbourne, Australia
Tue 22 Sep 2020 09:30 - 09:50 at Kangaroo - Formal Methods (2) Chair(s): Eunsuk Kang

Recent probabilistic model checking techniques can verify reliability and performance properties of software systems affected by parametric uncertainty. This involves modelling the system behaviour using \emph{interval Markov chains}, i.e., Markov models with transition probabilities or rates specified as intervals. These intervals can be updated continually using Bayesian estimators with imprecise priors, enabling the verification of the system properties of interest at runtime. However, Bayesian estimators are slow to react to sudden changes in the actual value of the estimated parameters, yielding inaccurate intervals and leading to poor verification results after such changes. To address this limitation, we introduce an efficient interval change-point detection method, and we integrate it with a state-of-the-art Bayesian estimator with imprecise priors. Our experimental results show that the resulting end-to-end Bayesian approach to change-point detection and estimation of interval Markov chain parameters handles effectively a wide range of sudden changes in parameter values, and supports runtime probabilistic model checking under parametric uncertainty.

Tue 22 Sep

Displayed time zone: (UTC) Coordinated Universal Time change

09:10 - 10:10
Formal Methods (2)Research Papers at Kangaroo
Chair(s): Eunsuk Kang Carnegie Mellon University, USA
09:10
20m
Talk
Verified from Scratch: Program Analysis for Learners' Programs
Research Papers
Andreas Stahlbauer University of Passau, Christoph Fr├Ądrich University of Passau, Gordon Fraser University of Passau
09:30
20m
Talk
Interval Change-Point Detection for Runtime Probabilistic Model Checking
Research Papers
Xingyu Zhao Heriot-Watt University, Radu Calinescu University of York, UK, Simos Gerasimou University of York, UK, Valentin Robu Heriot-Watt University, David Flynn Heriot-Watt University
Pre-print
09:50
20m
Talk
UnchartIt: An Interactive Framework for Program Recovery from Charts
Research Papers
Daniel Ramos INESC-ID/IST, Universidade de Lisboa, Jorge Pereira INESC-ID/IST, Universidade de Lisboa, Ines Lynce INESC-ID/IST, Universidade de Lisboa, Vasco Manquinho INESC-ID/IST, Universidade de Lisboa, Ruben Martins Carnegie Mellon University