State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Model Checking via Games
As one of the most successful formal methods, model checking has been widely used in the analysis and verification of concurrent systems. In this talk I will briefly review the basic ideas of model checking, then introduce a particular game, called parity game, which is equivalent to the problem of mu-calculus model checking. I will show that the set of the winning positions of a player can be naturally organised into a hierarchy of regions, which are strongly connected components in the game graph, with various degrees of closeness. The regions at the bottom level of the hierarchy are self-closed, while the regions at a higher level are closed with respect to those at lower levels. As a consequence, the problem of determining winning positions of parity games can be reduced to computing closed regions in game graphs.
Huimin Lin is a Research Professor in Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences. He has been an Academician of Chinese Academy of Sciences since 1999. He is primarily devoted to the research of formal semantics and formal methods of computer programs. He designed and realized the general process algebra validation tool PAM/VPAM, causing an important impact on the development of this kind of tools. In cooperation with Professor Hennessy from UK, Lin proposed and then independently developed the theory of Symbolic Bi-simulation, solving the problem that traditional concurrent computing models could not effectively simulate the large number of practical applications, and providing a theoretical basis for the inference and validation of communication concurrent processes. He also proposed the complete proof system and unique fixed-point induction for weak bi-simulation of the concurrent computing model Pi-Calculus, solving the problem of finite axiomatization of Pi-Calculus.
Department of Computer Science, University of Oxford
Probabilistic Programming for Bayesian Machine Learning
Probabilistic programming is a general-purpose means of expressing probabilistic models as computer programs, and automatically performing Bayesian inference such as posterior probability and marginalisation. By providing these model-based inference algorithms, probabilistic programming systems enable data scientists to focus on the design of good models, utilising their domain knowledge; the task of constructing efficient inference engines can be left to researchers with expertise in statistical machine learning and programming languages. By promoting the separation between model construction and inference procedures, probabilistic programming can democratise access to Bayesian machine learning. The full potential of probabilistic programming will come from automating the inference of latent variables in the model, conditioned on the observed data. Because of their generality, probabilistic programming poses interesting and challenging research problems for programming languages and the statistical foundations of machine learning. In this talk I will introduce probabilistic programming for Bayesian machine learning as a general concept, and explain a number of research directions unique to probabilistic programming.
Luke Ong is Professor of Computer Science and Head of Programming Languages Research, Department of Computer Science, University of Oxford; and Fellow of Merton College. He works in programming languages, verification, semantics of computation, and logic and algorithms. Ong has made pioneering contributions to game semantics; he has played a leading role in the development of higher-order model checking. His current research interests include statistical probabilistic programming for Bayesian machine learning and differentiable programming; specification and synthesis of programs; analysis of concurrent and distributed systems; and verification of cryptographic and consensus protocols. Ong was a joint winner of the 2017 ACM/EATCS Alonzo Church Award for Outstanding Contributions to Logic and Computation. He is a former General Chair of ACM/IEEE Symposium on Logic in Computer Science (LICS), and Vice Chair of the ACM Special Interest Group in Logic and Computation (SIGLOG). He has served on the steering committee of EATCS, EACSL, and ETAPS; and the judging panel of the EACSL Ackermann Award, EATCS Distinguished Dissertation Award, ETAPS / EATCS Best Paper Award, and ETAPS Test-of-Time Award. Ong has served on the editorial boards of Logical Methods in Computer Science, Mathematical Structures in Computer Science, and Acta Informatica.
School of Informatics, University of Edinburgh
Making Big Data Small
Big data analytics is often prohibitively costly. It is typically conducted by parallel processing with a cluster of machines, and is considered a privilege of big companies that can afford the resources. This talk argues that big data analytics is accessible to small companies with constrained resources. As an evidence, we present BEAS, a system for querying big data with bounded resources. BEAS advocates a resource-bounded query evaluation paradigm, based on a theory of bounded evaluation and a data-driven approximation scheme. As a proof of concept, BEAS is found to improve query evaluation of our industry collaborators by orders of magnitude.
Professor Wenfei Fan is the Chair of Web Data Management at the University of Edinburgh, UK, the Chief Scientist of Beijing Advanced Innovation Center for Big Data and Brain Computing (Beihang University), and the Chief Scientist of Shenzhen Institute of Computing Sciences, China. He is a Fellow of the Royal Society (FRS), a Fellow of the Royal Society of Edinburgh (FRSE), a Member of the Academy of Europe (MAE), an ACM Fellow (FACM), and a Yangtze River Scholar, China. He received his PhD from the University of Pennsylvania (USA), and his MSc and BSc from Peking University (China). He is a recipient of Royal Society Wolfson Research Merit Award in 2018, ERC Advanced Fellowship in 2015, the Roger Needham Award in 2008, the Outstanding Overseas Young Scholar Award in 2003 (China), the Career Award in 2001 (USA), a SIGMOD Research Highlight Award in 2018, and several Test-of-Time and Best Paper Awards, including the Alberto O. Mendelzon Test-of-Time Award of ACM PODS 2015 and 2010, Best Paper Awards for SIGMOD 2017, VLDB 2010, ICDE 2007 and Computer Networks 2002. His current research interests include database theory and systems, in particular big data, data quality, data integration, distributed query processing, query languages, recommender systems, social networks and Web services.