Stochasticity is commonly used to model and quantify uncertainty in systems, and infinite-state stochastic systems provide an expressive framework for modeling a wide range of applications. However, in contrast to their finite-state counterparts, formal verification of infinite-state stochastic systems is much less understood and is an active topic of research.
This talk will advocate for the use of martingale-based methods for formal verification of infinite-state stochastic systems. The key advantage of martingale-based methods is that they provide formal soundness and even a certain level of theoretical completeness guarantees, while allowing for fully automated verification algorithms for stochastic systems with applications in programming languages, control theory and artificial intelligence. In this talk, the speaker will present martingale-based methods for static analysis of probabilistic programs as well as for learning-based control and formal verification of learned policies in stochastic control systems. In particular, the talk will present some of the first methods for fully automated quantitative termination analysis in probabilistic programs and for learning-based control of stochastic systems with infinite time horizon guarantees.
About the Speaker
Djordje is a final year PhD student in computer science at the Institute of Science and Technology Austria (ISTA), under the supervision of Krishnendu Chatterjee and Petr Novotný. His research focuses on developing algorithms for formally verifying correctness of software and combines ideas from formal methods, programming languages and machine learning research as well as from probability theory. His research interests include stochastic system verification, static program analysis, learning-based control, neural network verification and bidding games. Prior to joining ISTA, he completed his bachelor's and master's degrees in mathematics at the University of Cambridge.
He is a tenure-track faculty candidate for the Information Systems & Technology, Software Engineering & Systems cluster.
