{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:00Z","timestamp":1787592240766,"version":"build-2736575974"},"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\/legalcode"}],"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 un-trusted 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\u2019s 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":2,"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6254-2388","authenticated-orcid":false,"given":"Jun","family":"Zhu","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","first-page":"22","volume-title":"Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017 (Proceedings of Machine Learning Research, Vol. 70)","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 (Proceedings of Machine Learning Research, Vol. 70), Doina Precup and Yee Whye Teh (Eds.). PMLR, 22\u201331. http:\/\/proceedings.mlr.press\/v70\/achiam17a.html"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V32I1.11797"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2014.2312453"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/ECC.2015.7330913"},{"key":"e_1_3_1_6_2","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"},{"key":"e_1_3_1_7_2","volume-title":"Introduction to probability","author":"Bertsekas Dimitri","year":"2008","unstructured":"Dimitri Bertsekas and John N Tsitsiklis. 2008. Introduction to probability. Vol. 1. Athena Scientific."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_4"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1146\/ANNUREV-CONTROL-042920-020211"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33013387"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.5555\/3463952.3464013"},{"key":"e_1_3_1_12_2","unstructured":"Yao Feng Jun Zhu Andr\u00e9 Platzer and Jonathan Laurent. 2025. Adaptive Shielding via Parametric Safety Proofs. arXiv:2502.18879 [cs.PL] https:\/\/arxiv.org\/abs\/2502.18879"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Yao Feng Jun Zhu Andr\u00e9 Platzer and Jonathan Laurent. 2025. Adaptive Shielding via Parametric Safety Proofs. doi:10.5281\/zenodo.14916164","DOI":"10.5281\/zenodo.14916164"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2018.2876389"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V32I1.12107"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_28"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.5555\/2789272.2886795"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Shangding Gu Long Yang Yali Du Guang Chen Florian Walter Jun Wang Yaodong Yang and Alois C. Knoll. 2022. A Review of Safe Reinforcement Learning: Methods Theory and Applications. CoRR abs\/2205.10330 (2022). doi:10.48550\/arXiv.2205.10330 arXiv:2205.10330","DOI":"10.48550\/arXiv.2205.10330"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2012.6225072"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3447928.3456653"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Radoslav Ivanov James Weimer Rajeev Alur George J Pappas and Insup Lee. 2019. Verisig: verifying safety properties of hybrid systems with neural network controllers. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. 169\u2013178. doi:10.1145\/3302504.3311806","DOI":"10.1145\/3302504.3311806"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_2"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2022.3197690"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/10187.001.0001"},{"issue":"1","key":"e_1_3_1_26_2","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_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2018.8619572"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_16"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01234-2_36"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0241-z"},{"key":"e_1_3_1_31_2","unstructured":"Randall Munroe. 2011. Significant. http:\/\/xkcd.com\/882\/."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9385-1"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78929-1_55"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_13"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","unstructured":"Andr\u00e9 Platzer and Yong Kiam Tan. 2018. Differential equation axiomatization: The impressive power of differential ghosts. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. 819\u2013828. doi:10.1145\/3209108.3209147","DOI":"10.1145\/3209108.3209147"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.23919\/ACC50511.2021.9482889"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10846-020-01183-3"},{"key":"e_1_3_1_39_2","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 http:\/\/arxiv.org\/abs\/1610.03295"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2002.1014237"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-020-00355-z"},{"key":"e_1_3_1_42_2","volume-title":"Reinforcement learning: An introduction","author":"Sutton Richard S","year":"2018","unstructured":"Richard S Sutton and Andrew G Barto. 2018. Reinforcement learning: An introduction. MIT press."},{"key":"e_1_3_1_43_2","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_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA46639.2022.9811698"},{"key":"e_1_3_1_45_2","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":[[2026,8,24]],"date-time":"2026-08-24T16:28:12Z","timestamp":1787588892000},"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":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}