Adaptive Shielding via Parametric Safety Proofs
This program is tentative and subject to change.
A major challenge to deploying cyber-physical systems with learning-enabled controllers is to ensure their safety, especially in the face of changing environments that necessitate runtime knowledge acquisition. Model-checking and automated reasoning have been successfully used for shielding, i.e., to monitor untrusted controllers and override potentially unsafe decisions, but only at the cost of hard tradeoffs in terms of expressivity, safety, adaptivity, precision and runtime efficiency. We propose a programming-language framework that allows experts to statically specify adaptive shields for learning-enabled agents, which enforce a safe control envelope that gets more permissive as knowledge is gathered at runtime. A shield specification provides a safety model that is parametric in the current agent’s knowledge. In addition, a nondeterministic inference strategy can be specified using a dedicated domain-specific language, enforcing that such knowledge parameters are inferred at runtime in a statistically-sound way. By leveraging language design and theorem proving, our proposed framework empowers experts to design adaptive shields with an unprecedented level of modeling flexibility, while providing rigorous, end-to-end probabilistic safety guarantees.
This program is tentative and subject to change.
Sat 18 OctDisplayed time zone: Perth change
13:45 - 15:30 | |||
13:45 15mTalk | Adaptive Shielding via Parametric Safety Proofs OOPSLA Yao Feng Tsinghua University, Jun Zhu Nankai University, André Platzer Karlsruhe Institute of Technology (KIT), Jonathan Laurent Carnegie Mellon University / Karlsruhe Institute of Technology | ||
14:00 15mTalk | Certified Decision Procedures for Width-Independent Bitvector Predicates OOPSLA Siddharth Bhat University of Cambridge, Leo Stefanesco University of Cambridge, Chris Hughes Independent Researcher, Tobias Grosser University of Cambridge | ||
14:15 15mTalk | Checking $\delta$-Satisfiability of Reals with Integrals OOPSLA Cody Rivera University of Illinois, Urbana-Champaign, Bishnu Bhusal University of Missouri, Rohit Chadha University of Missouri, A. Prasad Sistla University of Illinois at Chicago, Mahesh Viswanathan University of Illinois at Urbana-Champaign | ||
14:30 15mTalk | Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge OOPSLA John C. Kolesar Yale University, Shan Ali Yale University, Timos Antonopoulos Yale University, Ruzica Piskac Yale University | ||
14:45 15mTalk | Incremental Certified Programming OOPSLA Tomás Diaz University of Chile, Kenji Maillard Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile | ||
15:00 15mTalk | Pathological Cases for a Class of Reachability-Based Garbage Collectors OOPSLA Matthew Sotoudeh Stanford University Link to publication | ||
15:15 15mTalk | SafeTree: Expressive Tree Policies for Microservices OOPSLA |