{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T20:31:39Z","timestamp":1774729899808,"version":"3.50.1"},"reference-count":76,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,3,1]],"date-time":"2024-03-01T00:00:00Z","timestamp":1709251200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1646497"],"award-info":[{"award-number":["CCF-1646497"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1834324"],"award-info":[{"award-number":["CCF-1834324"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1834701"],"award-info":[{"award-number":["CNS-1834701"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1839511"],"award-info":[{"award-number":["CNS-1839511"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["IIS-1724341"],"award-info":[{"award-number":["IIS-1724341"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-2038853"],"award-info":[{"award-number":["CNS-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"}]},{"DOI":"10.13039\/100006602","name":"U.S. Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8650-16-C-2642"],"award-info":[{"award-number":["FA8650-16-C-2642"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"name":"International Science Partnerships Fund (ISPF) and the U.K. Research and Innovation through the EPSRC ECR International Collaboration Grants Program","award":["EP\/Y002644\/1"],"award-info":[{"award-number":["EP\/Y002644\/1"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1109\/tcad.2023.3331215","type":"journal-article","created":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T19:00:13Z","timestamp":1699470013000},"page":"994-1007","source":"Crossref","is-referenced-by-count":12,"title":["POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems"],"prefix":"10.1109","volume":"43","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0847-8570","authenticated-orcid":false,"given":"Yixuan","family":"Wang","sequence":"first","affiliation":[{"name":"Department of Electrical and Computer Engineering, Northwestern University, Evanston, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weichao","family":"Zhou","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Boston University, Boston, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9325-7718","authenticated-orcid":false,"given":"Jiameng","family":"Fan","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Boston University, Boston, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6645-262X","authenticated-orcid":false,"given":"Zhilu","family":"Wang","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Northwestern University, Evanston, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8989-7739","authenticated-orcid":false,"given":"Jiajun","family":"Li","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, U.K."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xin","family":"Chen","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of New Mexico, Albuquerque, NM, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9300-1787","authenticated-orcid":false,"given":"Chao","family":"Huang","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, U.K."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenchao","family":"Li","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Boston University, Boston, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7700-4099","authenticated-orcid":false,"given":"Qi","family":"Zhu","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Northwestern University, Evanston, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","article-title":"End to end learning for self-driving cars","author":"Bojarski","year":"2016","journal-title":"arXiv:1604.07316"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS54341.2022.00019"},{"key":"ref3","first-page":"39","article-title":"Safety-driven interactive planning for neural network-based lane changing","volume-title":"Proc. 28th Asia South Pacific Design Autom. Conf.","author":"Liu"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2016.7778091"},{"issue":"1","key":"ref5","first-page":"1334","article-title":"End-to-end training of deep visuomotor policies","volume":"17","author":"Levine","year":"2016","journal-title":"J. Mach. Learn. Res."},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3486611.3486644"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TSUSC.2019.2910533"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.2514\/6.2017-1743"},{"key":"ref9","first-page":"1","article-title":"Know the unknowns: Addressing disturbances and uncertainties in autonomous systems","volume-title":"Proc. 39th Int. Conf. Comput.- Aided Design","author":"Zhu"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1038\/nature14236"},{"key":"ref11","first-page":"1","article-title":"Enforcing hard constraints with soft barriers: Safe reinforcement learning in unknown stochastic environments","volume-title":"Proc. ICML","author":"Wang"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1015330.1015430"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2018.XIV.056"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3408308.3427617"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3358228"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311807"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311806"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"ref19","first-page":"10050","article-title":"Neural network control policy verification with persistent adversarial perturbation","volume-title":"Proc. ICML","author":"Wang"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3013071"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.23919\/DATE54114.2022.9774719"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2962027"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15956-5_1"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.29007\/zbkv"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.03.007"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883838"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(98)00193-9"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_44"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3126508"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2018.08.026"},{"key":"ref38","first-page":"1599","article-title":"Formal security analysis of neural networks using symbolic intervals","volume-title":"Proc. 27th USENIX Security Symp. (USENIX Security)","author":"Wang"},{"key":"ref39","first-page":"10802","article-title":"Fast and effective robustness certification","volume-title":"Proc. NeurIPS","author":"Singh"},{"key":"ref40","first-page":"1","article-title":"Beta-CROWN: Efficient bound propagation with perneuron split constraints for neural network robustness verification","volume-title":"Proc. NeurIPS","volume":"34","author":"Wang"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717716"},{"key":"ref42","first-page":"4944","article-title":"Efficient neural network robustness certification with general activation functions","volume-title":"Proc. NeurIPS","volume":"31","author":"Zhang"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_30"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_11"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/3419742"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19992-9_27"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_25"},{"key":"ref48","article-title":"Provably safe reinforcement learning via action projection using reachability analysis and polynomial zonotopes","author":"Kochdumper","year":"2022","journal-title":"arXiv:2210.10691"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i7.20790"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2020.3046193"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218742"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/3400302.3415676"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/3477031"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_6"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0249-6"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8431-1"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"ref58","first-page":"1","article-title":"Evaluating robustness of neural networks with mixed integer programming","volume-title":"Proc. ICLR","author":"Tjeng"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_18"},{"key":"ref60","article-title":"An approach to reachability analysis for feed-forward ReLU neural networks","author":"Lomuscio","year":"2017","journal-title":"arXiv:1706.07351v1"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/368"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1023\/A:1024467732637"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.70"},{"key":"ref65","article-title":"Reachability analysis of non-linear hybrid systems using Taylor models","author":"Chen","year":"2015"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2016.011"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461358"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0003-8"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1109\/AERO53065.2022.9843750"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0109720"},{"issue":"4","key":"ref71","first-page":"379","article-title":"Taylor models and other validated functional inclusion methods","volume":"4","author":"Makino","year":"2003","journal-title":"J. Pure Appl. Math."},{"key":"ref72","article-title":"Evaluating the robustness of neural networks: An extreme value theory approach","author":"Weng","year":"2018","journal-title":"arXiv:1801.10578"},{"key":"ref73","volume-title":"Bernstein Polynomials","author":"Lorentz","year":"2013"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1017\/S0013091500020101"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.29007\/x38n"},{"key":"ref76","article-title":"The third international verification of neural networks competition (VNN-COMP 2022): Summary and results","author":"M\u00fcller","year":"2022","journal-title":"arXiv:2212.10376"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/43\/10440374\/10312771-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/10440374\/10312771.pdf?arnumber=10312771","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,14]],"date-time":"2024-03-14T04:19:24Z","timestamp":1710389964000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10312771\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3]]},"references-count":76,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2023.3331215","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3]]}}}