{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T07:18:49Z","timestamp":1768288729036,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314638","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"686-701","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":50,"title":["An inductive synthesis framework for verifiable reinforcement learning"],"prefix":"10.1145","author":[{"given":"He","family":"Zhu","sequence":"first","affiliation":[{"name":"Galois, USA"}]},{"given":"Zikang","family":"Xiong","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Stephen","family":"Magill","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Control-Oriented Learning of Lagrangian and Hamiltonian Systems. In American Control Conference.","author":"Ahmadi M.","unstructured":"M. Ahmadi , C. Rowley , and U. Topcu . 2018 . Control-Oriented Learning of Lagrangian and Hamiltonian Systems. In American Control Conference. M. Ahmadi, C. Rowley, and U. Topcu. 2018. Control-Oriented Learning of Lagrangian and Hamiltonian Systems. In American Control Conference."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039601"},{"key":"e_1_3_2_2_3_1","first-page":"1424","volume-title":"53rd IEEE Conference on Decision and Control, CDC 2014","author":"Akametalu Anayo K.","year":"2014","unstructured":"Anayo K. Akametalu , Shahab Kaynama , Jaime F. Fisac , Melanie Nicole Zeilinger , Jeremy H. Gillula , and Claire J. Tomlin . 2014. Reachability-based safe learning with Gaussian processes . In 53rd IEEE Conference on Decision and Control, CDC 2014 , Los Angeles, CA, USA , December 15-17, 2014 . 1424 - 1431 . Anayo K. Akametalu, Shahab Kaynama, Jaime F. Fisac, Melanie Nicole Zeilinger, Jeremy H. Gillula, and Claire J. Tomlin. 2014. Reachability-based safe learning with Gaussian processes. In 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014. 1424-1431."},{"key":"e_1_3_2_2_4_1","volume-title":"Safe Reinforcement Learning via Shielding. AAAI","author":"Alshiekh Mohammed","year":"2018","unstructured":"Mohammed Alshiekh , Roderick Bloem , R\u00fcdiger Ehlers , Bettina K\u00f6nighofer , Scott Niekum , and Ufuk Topcu . 2018. Safe Reinforcement Learning via Shielding. AAAI ( 2018 ). Mohammed Alshiekh, Roderick Bloem, R\u00fcdiger Ehlers, Bettina K\u00f6nighofer, Scott Niekum, and Ufuk Topcu. 2018. Safe Reinforcement Learning via Shielding. AAAI (2018)."},{"key":"e_1_3_2_2_5_1","volume-title":"Dependable Software Systems Engineering. NATO Science for Peace and Security Series, D: Information and Communication Security","author":"Alur Rajeev","unstructured":"Rajeev Alur , Rastislav Bod\u00edk , Eric Dallal , Dana Fisman , Pranav Garg , Garvit Juniwal , Hadas Kress-Gazit , P. Madhusudan , Milo M. K. Martin , Mukund Raghothaman , Shambwaditya Saha , Sanjit A. Seshia , Rishabh Singh , Armando Solar-Lezama , Emina Torlak , and Abhishek Udupa . 2015. Syntax-Guided Synthesis . In Dependable Software Systems Engineering. NATO Science for Peace and Security Series, D: Information and Communication Security , Vol. 40 . IOS Press , 1-25. Rajeev Alur, Rastislav Bod\u00edk, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2015. Syntax-Guided Synthesis. In Dependable Software Systems Engineering. NATO Science for Peace and Security Series, D: Information and Communication Security, Vol. 40. IOS Press, 1-25."},{"key":"e_1_3_2_2_6_1","unstructured":"MOSEK ApS. 2018. The mosek optimization software. http:\/\/www.mosek.com  MOSEK ApS. 2018. The mosek optimization software . http:\/\/www.mosek.com"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Somil Bansal Mo Chen Sylvia Herbert and Claire J Tomlin. 2017. Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances. (2017).  Somil Bansal Mo Chen Sylvia Herbert and Claire J Tomlin. 2017. Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances. (2017).","DOI":"10.1109\/CDC.2017.8263977"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/3157382.3157391"},{"key":"e_1_3_2_2_9_1","volume-title":"Verifiable Reinforcement Learning via Policy Extraction. CoRR abs\/1805.08328","author":"Bastani Osbert","year":"2018","unstructured":"Osbert Bastani , Yewen Pu , and Armando Solar-Lezama . 2018. Verifiable Reinforcement Learning via Policy Extraction. CoRR abs\/1805.08328 ( 2018 ). Osbert Bastani, Yewen Pu, and Armando Solar-Lezama. 2018. Verifiable Reinforcement Learning via Policy Extraction. CoRR abs\/1805.08328 (2018)."},{"key":"e_1_3_2_2_10_1","volume-title":"Assessment of insulin sensitivity in vivo. Endocrine reviews 6, 1","author":"Bergman Richard N","year":"1985","unstructured":"Richard N Bergman , Diane T Finegood , and Marilyn Ader . 1985. Assessment of insulin sensitivity in vivo. Endocrine reviews 6, 1 ( 1985 ), 45-86. Richard N Bergman, Diane T Finegood, and Marilyn Ader. 1985. Assessment of insulin sensitivity in vivo. Endocrine reviews 6, 1 (1985), 45-86."},{"key":"e_1_3_2_2_11_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","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. 908- 919. 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. 908- 919."},{"key":"e_1_3_2_2_12_1","first-page":"533","volume-title":"TACAS","author":"Bloem Roderick","year":"2015","unstructured":"Roderick Bloem , Bettina K\u00f6nighofer , Robert K\u00f6nighofer , and Chao Wang . 2015 . Shield Synthesis: - Runtime Enforcement for Reactive Systems. In Tools and Algorithms for the Construction and Analysis of Systems - 21-t International Conference , TACAS 2015. 533 - 548 . Roderick Bloem, Bettina K\u00f6nighofer, Robert K\u00f6nighofer, and Chao Wang. 2015. Shield Synthesis: - Runtime Enforcement for Reactive Systems. In Tools and Algorithms for the Construction and Analysis of Systems - 21-t International Conference, TACAS 2015. 533-548."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_14_1","volume-title":"Linear-Quadratic Control: An Introduction","author":"Dorato Peter","unstructured":"Peter Dorato , Vito Cerone , and Chaouki Abdallah . 1994. Linear-Quadratic Control: An Introduction . Simon & Schuster, Inc. , New York, NY, USA . Peter Dorato, Vito Cerone, and Chaouki Abdallah. 1994. Linear-Quadratic Control: An Introduction. Simon & Schuster, Inc., New York, NY, USA."},{"key":"e_1_3_2_2_15_1","first-page":"347","volume-title":"CAV","author":"Fan Chuchu","year":"2018","unstructured":"Chuchu Fan , Umang Mathur , Sayan Mitra , and Mahesh Viswanathan . 2018 . Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics. In Computer Aided Verification - 30th International Conference , CAV 2018. 347 - 366 . Chuchu Fan, Umang Mathur, Sayan Mitra, and Mahesh Viswanathan. 2018. Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics. In Computer Aided Verification - 30th International Conference, CAV 2018. 347-366."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCA.2016.7587949"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_2_2_18_1","volume-title":"IEEE International Conference on Robotics and Automation, ICRA 2012","author":"Jeremy","year":"2012","unstructured":"Jeremy H. Gillula and Claire J. Tomlin. 2012. Guaranteed Safe Online Learning via Reachability: tracking a ground target using a quadrotor . In IEEE International Conference on Robotics and Automation, ICRA 2012 , 14-18 May , 2012 , St. Paul, Minnesota, USA. 2723-2730. Jeremy H. Gillula and Claire J. Tomlin. 2012. Guaranteed Safe Online Learning via Reachability: tracking a ground target using a quadrotor. In IEEE International Conference on Robotics and Automation, ICRA 2012, 14-18 May, 2012, St. Paul, Minnesota, USA. 2723-2730."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"e_1_3_2_2_21_1","volume-title":"CAV (1) (Lecture Notes in Computer Science)","author":"Huang Xiaowei","unstructured":"Xiaowei Huang , Marta Kwiatkowska , Sen Wang , and Min Wu. 2017. Safety Verification of Deep Neural Networks . In CAV (1) (Lecture Notes in Computer Science) , Vol. 10426 . 3-29. Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety Verification of Deep Neural Networks. In CAV (1) (Lecture Notes in Computer Science), Vol. 10426. 3-29."},{"key":"e_1_3_2_2_22_1","unstructured":"Dominic W Jordan and Peter Smith. 1987. Nonlinear ordinary differential equations. (1987).   Dominic W Jordan and Peter Smith. 1987. Nonlinear ordinary differential equations. (1987)."},{"key":"e_1_3_2_2_23_1","first-page":"97","volume-title":"CAV","author":"Katz Guy","year":"2017","unstructured":"Guy Katz , Clark W. Barrett , David L. Dill , Kyle Julian , and Mykel J. Kochenderfer . 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Computer Aided Verification - 29th International Conference , CAV 2017 . 97 - 117 . Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Computer Aided Verification - 29th International Conference, CAV 2017. 97-117."}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314638","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314638","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314638","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314638"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":23,"alternative-id":["10.1145\/3314221.3314638","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314638","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}