Adaptive Shielding via Parametric Safety Proofs
summary
A programming-language framework implements parametric safety proofs that let a shield start conservative and become permissive as runtime knowledge is inferred, producing compiled proof obligations and RL-ready shield code. It uses Differential Dynamic Logic for hybrid models and a DSL for statistically sound inference of environment parameters, yields formal end-to-end probabilistic safety guarantees, keeps training and testing accident-free while matching unshielded returns, and reports ≤15% runtime overhead with artifacts reproduced.
AI-written summary · about
chapters (9)
- 0:00Adaptive shielding intro
- 1:27Static shielding limits
- 5:03Adaptive shielding challenges
- 6:06Programming language framework
- 8:58Controller updates policy
- 10:20Parametric safety proofs
- 11:47Proof obligations automation
- 12:08Experimental results
- 13:00Q&A
related talks
20mThe Challenges in Supporting Multiple Safety Levels in the Same System
21mDeductive Verification of Parameterized Embedded Systems modeled in SystemC
19mModular Hardware Design of Pipelined Circuits with Hazards
08mEmbedded Executive LIVE
06mRISC-V Spotlight: Avoiding Murphy's Law and Satan's Law Without Selling your Soul
24mBioScript: Programming Safe Chemistry on Laboratories-on-a-Chip
01h 10mHardware DSLs
20mOpen Source Safety Elements - Out of Context?