{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:16:23Z","timestamp":1750220183798,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,7,10]],"date-time":"2022-07-10T00:00:00Z","timestamp":1657411200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1834701, 1724341, 2038853"],"award-info":[{"award-number":["1834701, 1724341, 2038853"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-19-1-2496"],"award-info":[{"award-number":["N00014-19-1-2496"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,7,10]]},"DOI":"10.1145\/3489517.3530556","type":"proceedings-article","created":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T23:19:29Z","timestamp":1661296769000},"page":"925-930","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Design-while-verify"],"prefix":"10.1145","author":[{"given":"Yixuan","family":"Wang","sequence":"first","affiliation":[{"name":"Northwestern University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Huang","sequence":"additional","affiliation":[{"name":"Liverpool University, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhaoran","family":"Wang","sequence":"additional","affiliation":[{"name":"Northwestern University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhilu","family":"Wang","sequence":"additional","affiliation":[{"name":"Northwestern University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qi","family":"Zhu","sequence":"additional","affiliation":[{"name":"Northwestern University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,23]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Martin Arjovsky Soumith Chintala and L\u00e9on Bottou. 2017. Wasserstein generative adversarial networks. In ICML. PMLR."},{"key":"e_1_3_2_1_2_1","volume-title":"The explicit linear quadratic regulator for constrained systems. Automatica","author":"Bemporad Alberto","year":"2002","unstructured":"Alberto Bemporad, Manfred Morari, Vivek Dua, and Efstratios N Pistikopoulos. 2002. The explicit linear quadratic regulator for constrained systems. Automatica (2002)."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(00)00050-9"},{"volume-title":"Flow*: An analyzer for non-linear hybrid systems","author":"Chen Xin","key":"e_1_3_2_1_4_1","unstructured":"Xin Chen, Erika \u00c1brah\u00e1m, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In CAV. Springer, 258--263."},{"volume-title":"Robust reach-avoid controller synthesis for switched nonlinear systems","author":"Ding Jerry","key":"e_1_3_2_1_5_1","unstructured":"Jerry Ding and Claire J Tomlin. 2010. Robust reach-avoid controller synthesis for switched nonlinear systems. In CDC. IEEE, 6481--6486."},{"key":"e_1_3_2_1_6_1","volume-title":"Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems","author":"Dreossi Tommaso","year":"2019","unstructured":"Tommaso Dreossi, Daniel J Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit Seshia. 2019. Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems. In CAV. Springer, 432--442."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Souradeep Dutta Xin Chen and Sriram Sankaranarayanan. 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In HSCC. 157--168.","DOI":"10.1145\/3302504.3311807"},{"key":"e_1_3_2_1_8_1","volume-title":"Controller synthesis for linear system with reach-avoid specifications","author":"Fan Chuchu","year":"2021","unstructured":"Chuchu Fan, Zengyi Qin, Umang Mathur, Qiang Ning, Sayan Mitra, and Mahesh Viswanathan. 2021. Controller synthesis for linear system with reach-avoid specifications. IEEE Trans. Automat. Control (2021)."},{"key":"e_1_3_2_1_9_1","unstructured":"Jiameng Fan Chao Huang Xin Chen Wenchao Li and Qi Zhu. 2020. ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems. In ATVA Dang Van Hung and Oleg Sokolsky (Eds.). Springer International Publishing."},{"key":"e_1_3_2_1_10_1","first-page":"2944","article-title":"Learning Continuous Control Policies by Stochastic Value Gradients","volume":"28","author":"Heess Nicolas","year":"2015","unstructured":"Nicolas Heess, Gregory Wayne, David Silver, Timothy Lillicrap, Tom Erez, and Yuval Tassa. 2015. Learning Continuous Control Policies by Stochastic Value Gradients. NIPs 28 (2015), 2944--2952.","journal-title":"NIPs"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Peter Henderson Riashat Islam Philip Bachman Joelle Pineau Doina Precup and David Meger. 2018. Deep reinforcement learning that matters. In AAAI.","DOI":"10.1609\/aaai.v32i1.11694"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_3_2_1_13_1","unstructured":"Kai-Chieh Hsu Vicen\u00e7 Rubies-Royo Claire J Tomlin and Jaime F Fisac. 2021. Safety and Liveness Guarantees through Reach-Avoid Reinforcement Learning. In Robotics: Science and Systems."},{"key":"e_1_3_2_1_14_1","volume-title":"POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems. arXiv preprint arXiv:2106.13867","author":"Huang Chao","year":"2021","unstructured":"Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li, and Qi Zhu. 2021. POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems. arXiv preprint arXiv:2106.13867 (2021)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3358228"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Radoslav Ivanov Taylor J Carpenter James Weimer Rajeev Alur George J Pappas and Insup Lee. 2020. Case study: verifying the safety of an autonomous racing car with a neural network controller. In HSCC. 1--7.","DOI":"10.1145\/3365365.3382216"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","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 HSCC. 169--178.","DOI":"10.1145\/3302504.3311806"},{"key":"e_1_3_2_1_18_1","unstructured":"Timothy P Lillicrap Jonathan J Hunt Alexander Pritzel Nicolas Heess Tom Erez Yuval Tassa David Silver and Daan Wierstra. 2016. Continuous control with deep reinforcement learning.. In ICLR (Poster)."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Gabriel Peyr\u00e9 Marco Cuturi et al. 2019. Computational optimal transport: With applications to data science. Foundations and Trends\u00ae in Machine Learning 11 5--6 (2019) 355--607.","DOI":"10.1561\/2200000073"},{"key":"e_1_3_2_1_20_1","volume-title":"Provably Correct Training of Neural Network Controllers Using Reachability Analysis. arXiv preprint","author":"Sun Xiaowu","year":"2021","unstructured":"Xiaowu Sun and Yasser Shoukry. 2021. Provably Correct Training of Neural Network Controllers Using Reachability Analysis. arXiv preprint (2021)."},{"key":"e_1_3_2_1_21_1","volume-title":"Cocktail: Learn a Better Neural Network Controller from Multiple Experts via Adaptive Mixing and Robust Distillation. DAC","author":"Wang Yixuan","year":"2021","unstructured":"Yixuan Wang, Chao Huang, Zhilu Wang, Shichao Xu, Zhaoran Wang, and Qi Zhu. 2021. Cocktail: Learn a Better Neural Network Controller from Multiple Experts via Adaptive Mixing and Robust Distillation. DAC (2021)."},{"volume-title":"Energy-efficient control adaptation with safety guarantees for learning-enabled cyber-physical systems","author":"Wang Yixuan","key":"e_1_3_2_1_22_1","unstructured":"Yixuan Wang, Chao Huang, and Qi Zhu. 2020. Energy-efficient control adaptation with safety guarantees for learning-enabled cyber-physical systems. In ICCAD. IEEE, 1--9."},{"key":"e_1_3_2_1_23_1","unstructured":"Webots. [n. d.]. http:\/\/www.cyberbotics.com. Mobile Robot Simulation Software."}],"event":{"name":"DAC '22: 59th ACM\/IEEE Design Automation Conference","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE CEDA"],"location":"San Francisco California","acronym":"DAC '22"},"container-title":["Proceedings of the 59th ACM\/IEEE Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3489517.3530556","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3489517.3530556","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3489517.3530556","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:18Z","timestamp":1750186938000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3489517.3530556"}},"subtitle":["correct-by-construction control learning with verification in the loop"],"short-title":[],"issued":{"date-parts":[[2022,7,10]]},"references-count":23,"alternative-id":["10.1145\/3489517.3530556","10.1145\/3489517"],"URL":"https:\/\/doi.org\/10.1145\/3489517.3530556","relation":{},"subject":[],"published":{"date-parts":[[2022,7,10]]},"assertion":[{"value":"2022-08-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}