Invited speakers
Automating Proof Rules for Probabilistic Programs
Over the last 15+ years, probabilistic programs have received much attention. By now, there exists a plethora of proof rules for quantifying, amongst others, the termination probability or expected runtimes of such programs. Those rules must be adapted and combined to enable the verification of feature-rich probabilistic programming languages. In this talk, I will discuss ongoing work on developing an intermediate verification infrastructure for automating proof rules for probabilistic programs.
Christoph Matheja
Professor in Computer Science
University of Oldenburg, Germany
DTU Technical University of Denmark, Denmark
Christoph Matheja is a Professor at the University of Oldenburg and an associate professor at the Technical University of Denmark. His research interests include deductive verification techniques and model checking of probabilistic and heap-manipulating systems.
Neural synthesis for verification and control of stochastic systems - certificates and abstractions
Concerned with general temporal specifications over dynamical models and reactive programs, I discuss how sound synthesis plays a central role for the formal verification of stochastic systems.
Verification can be attained via synthesis either of certificates based on proof rules, or of formal abstractions. For both problems, I discuss two separate approaches, the first (constructive) based on full knowledge of models, the latter (inductive) leveraging samples from their dynamics and the training of neural nets.
In the context of sequential decision making problems over stochastic systems, I additionally discuss how to generate policies/strategies/controllers, in order to formally attain given specifications, again with model-based and data-driven techniques.
Alessandro Abate
Professor in Computer Science
University of Oxford, UK
Alessandro Abate is Professor of Verification and Control in the Department of Computer Science at the University of Oxford. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control, TU Delft. He received Laurea-MS/PhD degrees from the University of Padua and UC Berkeley.
Runtime Safety for Learning-Enabled Cyber-Physical Systems: From Predictive Monitoring to Adaptive Shielding
The rise of learning-enabled cyber-physical systems (CPS) in safety-critical domains calls for novel runtime safety assurance mechanisms. This talk presents our recent work in logic-guided predictive monitoring and adaptive shielding as foundational techniques for safeguarding learning-enabled CPS at runtime. We explore a range of systems employing various learning components: from monitoring sequential predictions generated by Bayesian Recurrent Neural Networks to shielding unsafe actions in reinforcement learning for multi-agent interactions, partially observable environments, and settings with hidden parameter variations. Extensive case studies in robotics, healthcare, and smart cities illustrate the potential impact of our methods, paving the way for safe and trustworthy learning-enabled CPS.
Lu Feng
Associate Professor in Computer Science
University of Virginia, USA
Lu Feng is an Associate Professor of Computer Science at the University of Virginia, USA. She holds a D.Phil. in Computer Science from the University of Oxford. Her research bridges formal methods, machine learning, and human-autonomy interaction to advance the development of learning-enabled cyber-physical systems that are provably correct and aligned with human values. Her work spans a range of application domains, including robotics, autonomous driving, medical devices, and smart cities. Dr. Feng serves as an Associate Editor for the ACM Transactions on Cyber-Physical Systems and is a steering committee member of the ACM/IEEE Conference on Cyber-Physical Systems.