All times are given in Beijing time (UTC+08:00)

Day 1 (November 25, 2021)

Day 2 (November 26, 2021)

Day 3 (November 27, 2021)

Prof. Joost-Pieter Katoen: Mechanically Finding the Right Probabilities in Markov Models

Markov chains are central in performance and dependability analysis, whereas Markov decision processes are key in stochastic decision making and planning in AI. A standard assumption in these models is that all probabilities are precisely known a priori. In many cases, this assumption is too severe. System quantities such as component fault rates, molecule reaction rates, packet loss ratios, etc. are often not, or at best partially, known.

This talk surveys the analysis of parametric Markov models whose transitions are labelled with functions over a finite set of parameters. These models are symbolic representations of uncountably many concrete probabilistic models, each obtained by instantiating the parameters.

We consider various analysis problems for a given logical specification φ: do all parameter instantiations within a given region of parameter values satisfy φ?, which instantiations satisfy φ and which ones do not?, and how can all such instantiations be characterised, either exactly or approximately?

We address theoretical complexity results and describe the main ideas underlying state-of-the-art algorithms that established an impressive leap over the last decade enabling the fully automated analysis of models with millions of states and thousands of parameters. Examples from distributed computing, satellites and AI illustrate the applicability of these parameter synthesis techniques.

Prof. Frits Vaandrager: A New Approach for Active Automata Learning Based on Apartness

We present L^#, a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the L^ast algorithm and its descendants, L^# takes a different perspective: it tries to establish apartness, a constructive form of inequality. L^# does not require auxiliary notions such as observation tables or discrimination trees, but operates directly on tree-shaped automata. L^# has the same asymptotic query and symbol complexities as the best existing learning algorithms, but we show that adaptive distinguishing sequences can be naturally integrated to boost the performance of L^# in practice. Experiments with a prototype implementation, written in Rust, suggest that L^# outperforms existing algorithms.
(Joint work with Bharat Garhewal, Jurriaan Rot & Thorsten Wissmann.)

Prof. Charles Zhang: Enterprise-Scale Static Analysis: A Pinpoint Experience

Despite years of research and practice, modern static analysis techniques still cannot detect oldest and extremely well understood software bugs such as the Heartbleed, one of the most "spectacular" security flaws of the recent decade. A remedy, as what we have attempted through the successful commercialization of the Pinpoint platform (PLDI 18), is to make static program analysis aware of the basic characteristics of the modern enterprise-scale software system. The talk focuses on discussing these characteristics and how Pinpoint addresses them pragmatically as well as its future directions. Pinpoint is a LLVM-based cross-language static analysis platform and deployed in major Chinese tech companies such as Tencent, Baidu, Huawei, and Alibaba.