Probabilistic systems have increasingly become ubiquitous in many areas of computer science, including security protocols, artificial intelligence, planning and control, network analysis, and robotics, to name a few. To deploy them in practice, we must have formal and rigorous mathematical guarantees about the behavior of such systems. Formal methods are a well-known paradigm concerned with verification and correct-by-construction in design of software systems. The design and utilization of formal methods for probabilistic models and programs will enable researchers as well as practitioners to design software and intelligent systems that are more robust, trustworthy and safe, even in the presence of probabilistic uncertainty.
The goal of this meeting is to bring together international experts from all over the world in the areas of formal methods, program verification, probabilistic AI, reinforcement learning, Markov chains and Markov decision processes, who all build algorithmic and logical tools with mathematical guarantees for probabilistic systems. Our aim is to create synergy between different communities who share much of the theoretical and mathematical foundations of their research, but are otherwise quite separate, and to create an environment in which they can interchange ideas and learn about the most recent advances in each other’s fields. We believe and hope that this will help forge many new interdisciplinary collaborations and significantly benefit both the attendees and their research communities at large. Our goal is to also foster new collaborations on the area of probabilistic verification between top universities across Asia.
The meeting will focus on some of the most challenging problems in all of computer science which form the frontiers of probabilistic models and programs, by focusing on introducing the most novel and recent ideas on formal reasoning about probabilistic systems. Some particular topics of focus will be as follows:
Reasoning about large and infinite-state probabilistic models, e.g. probabilistic programs
Parametrized algorithms for reasoning about probabilistic models
Data-driven and certified learning approaches for probabilistic models
Compositional reasoning about probabilistic models
Distributional view of probabilistic verification
By featuring invited talks from some of the top international researchers in all the directions above, as well as group discussions and problem-solving sessions, we hope to provide an opportunity for the participants to broaden their exposure to new and unconventional results which lie outside of their comfort zones and have the potential for high-risk high-reward research.