{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:05:12Z","timestamp":1760058312814,"version":"build-2065373602"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n            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\n            <jats:italic toggle=\"yes\">adaptive shields<\/jats:italic>\n            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.\n          <\/jats:p>","DOI":"10.1145\/3720450","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"816-843","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Adaptive Shielding via Parametric Safety Proofs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8213-5181","authenticated-orcid":false,"given":"Yao","family":"Feng","sequence":"first","affiliation":[{"name":"Tsinghua University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6254-2388","authenticated-orcid":false,"given":"Jun","family":"Zhu","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Karlsruhe, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8477-1560","authenticated-orcid":false,"given":"Jonathan","family":"Laurent","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Karlsruhe, Germany"},{"name":"Carnegie Mellon University, Pittsburgh, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 34th International Conference on Machine Learning, ICML 2017","author":"Achiam Joshua","year":"2017","unstructured":"Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel. 2017. Constrained Policy Optimization. In Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017, Doina Precup and Yee Whye Teh (Eds.) (Proceedings of Machine Learning Research, Vol. 70). PMLR, 22\u201331. http:\/\/proceedings.mlr.press\/v70\/achiam17a.html"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V32I1.11797"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2014.2312453"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECC.2015.7330913"},{"key":"e_1_2_1_5_1","volume-title":"Safe Model-based Reinforcement Learning with Stability Guarantees. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017","author":"Berkenkamp Felix","year":"2017","unstructured":"Felix Berkenkamp, Matteo Turchetta, Angela P. Schoellig, and Andreas Krause. 2017. Safe Model-based Reinforcement Learning with Stability Guarantees. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (Eds.). 908\u2013918. https:\/\/proceedings.neurips.cc\/paper\/2017\/hash\/766ebcd59621e305170616ba3d3dac32-Abstract.html"},{"volume-title":"Introduction to probability. 1","author":"Bertsekas Dimitri","key":"e_1_2_1_6_1","unstructured":"Dimitri Bertsekas and John N Tsitsiklis. 2008. Introduction to probability. 1, Athena Scientific."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_4"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1146\/ANNUREV-CONTROL-042920-020211"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33013387"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/3463952.3464013"},{"key":"e_1_2_1_11_1","unstructured":"Yao Feng Jun Zhu Andr\u00e9 Platzer and Jonathan Laurent. 2025. Adaptive Shielding via Parametric Safety Proofs. arxiv:2502.18879. arxiv:2502.18879"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Yao Feng Jun Zhu Andr\u00e9 Platzer and Jonathan Laurent. 2025. Adaptive Shielding via Parametric Safety Proofs. https:\/\/doi.org\/10.5281\/zenodo.14916164 10.5281\/zenodo.14916164","DOI":"10.5281\/zenodo.14916164"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2018.2876389"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V32I1.12107"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_28"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2789272.2886795"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2205.10330"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2012.6225072"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3447928.3456653"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311806"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_2"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2022.3197690"},{"volume-title":"Decision making under uncertainty: theory and application","author":"Kochenderfer Mykel J","key":"e_1_2_1_24_1","unstructured":"Mykel J Kochenderfer. 2015. Decision making under uncertainty: theory and application. MIT press."},{"key":"e_1_2_1_25_1","first-page":"17","article-title":"Next generation airborne collision avoidance system","volume":"19","author":"Kochenderfer Mykel J","year":"2012","unstructured":"Mykel J Kochenderfer, Jessica E Holland, and James P Chryssanthacopoulos. 2012. Next generation airborne collision avoidance system. Lincoln Laboratory Journal, 19, 1 (2012), 17\u201333.","journal-title":"Lincoln Laboratory Journal"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2018.8619572"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_16"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01234-2_36"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0241-z"},{"key":"e_1_2_1_30_1","unstructured":"Randall Munroe. 2011. Significant. http:\/\/xkcd.com\/882\/"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9385-1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78929-1_55"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_13"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209147"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.23919\/ACC50511.2021.9482889"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10846-020-01183-3"},{"key":"e_1_2_1_38_1","volume-title":"Reinforcement Learning for Autonomous Driving. CoRR, abs\/1610.03295","author":"Shalev-Shwartz Shai","year":"2016","unstructured":"Shai Shalev-Shwartz, Shaked Shammah, and Amnon Shashua. 2016. Safe, Multi-Agent, Reinforcement Learning for Autonomous Driving. CoRR, abs\/1610.03295 (2016), arXiv:1610.03295. arxiv:1610.03295"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2002.1014237"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-020-00355-z"},{"volume-title":"Reinforcement learning: An introduction","author":"Sutton Richard S","key":"e_1_2_1_41_1","unstructured":"Richard S Sutton and Andrew G Barto. 2018. Reinforcement learning: An introduction. MIT press."},{"key":"e_1_2_1_42_1","volume-title":"Reward Constrained Policy Optimization. In 7th International Conference on Learning Representations, ICLR 2019","author":"Tessler Chen","year":"2019","unstructured":"Chen Tessler, Daniel J. Mankowitz, and Shie Mannor. 2019. Reward Constrained Policy Optimization. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net. https:\/\/openreview.net\/forum?id=SkfrvsA9FX"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA46639.2022.9811698"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V35I12.17272"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720450","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720450","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:06:14Z","timestamp":1760029574000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720450"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":44,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720450"],"URL":"https:\/\/doi.org\/10.1145\/3720450","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}