{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:34Z","timestamp":1779087694172,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,6,23]],"date-time":"2024-06-23T00:00:00Z","timestamp":1719100800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,6,23]]},"DOI":"10.1145\/3649329.3658256","type":"proceedings-article","created":{"date-parts":[[2024,11,7]],"date-time":"2024-11-07T19:27:22Z","timestamp":1731007642000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Neural Barrier Certificates Synthesis of NN-Controlled Continuous Systems via Counterexample-Guided Learning"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5246-0330","authenticated-orcid":false,"given":"Hanrui","family":"Zhao","sequence":"first","affiliation":[{"name":"East China Normal University, Shanghai, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5352-3681","authenticated-orcid":false,"given":"Niuniu","family":"Qi","sequence":"additional","affiliation":[{"name":"East China normal University, Shanghai, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3772-8369","authenticated-orcid":false,"given":"Mengxin","family":"Ren","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2575-7045","authenticated-orcid":false,"given":"Xia","family":"Zeng","sequence":"additional","affiliation":[{"name":"Southwest University, Chongqing, Chongqing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9728-1114","authenticated-orcid":false,"given":"Zhenbing","family":"Zeng","sequence":"additional","affiliation":[{"name":"Shanghai University, Shanghai, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1209-8191","authenticated-orcid":false,"given":"Zhengfeng","family":"Yang","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,11,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3447928.3456646"},{"key":"e_1_3_2_1_2_1","volume-title":"Handbook of Satisfiability","author":"Barrett Clark","unstructured":"Clark Barrett, Roberto Sebastiani, Sanjit A Seshia, and Cesare Tinelli. 2021. Satisfiability Modulo Theories. In Handbook of Satisfiability (second ed.). IOS Press."},{"key":"e_1_3_2_1_3_1","volume-title":"A novel approach for solving the BMI problem in barrier certificates generation","author":"Chen Xin","unstructured":"Xin Chen, Chao Peng, Wang Lin, Zhengfeng Yang, Yifang Zhang, and Xuandong Li. 2020. A novel approach for solving the BMI problem in barrier certificates generation. In Proceedings of CAV. Springer, 582--603."},{"key":"e_1_3_2_1_4_1","first-page":"1846","article-title":"Computing output feedback controllers to enlarge the domain of attraction in polynomial systems","volume":"49","author":"Chesi G.","year":"2004","unstructured":"G. Chesi. 2004. Computing output feedback controllers to enlarge the domain of attraction in polynomial systems. IEEE TAC 49, 10 (2004), 1846--1853.","journal-title":"IEEE TAC"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Jyotirmoy V. Deshmukh James P. Kapinski Tomoya Yamaguchi and Danil Prokhorov. 2019. Learning Deep Neural Network Controllers for Dynamical Systems with Safety Guarantees: Invited Paper. In 2019 IEEE\/ACM ICCAD. 1--7.","DOI":"10.1109\/ICCAD45719.2019.8942130"},{"key":"e_1_3_2_1_6_1","volume-title":"Advances in NIPS","volume":"32","author":"Fazlyab Mahyar","year":"2019","unstructured":"Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George Pappas. 2019. Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks. In Advances in NIPS, Vol. 32."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 24th CADE. 208--214","author":"Gao Sicun","unstructured":"Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. dReal: An SMT Solver for Nonlinear Theories over the Reals. In Proceedings of the 24th CADE. 208--214."},{"key":"e_1_3_2_1_8_1","unstructured":"Gao Sicun. 2016. Quadcopter model. https:\/\/github.com\/dreal\/benchmarks."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Edda Klipp Ralf Herwig Axel Kowald Christoph Wierling and Hans Lehrach. 2005. Systems biology in practice: concepts implementation and application.","DOI":"10.1002\/3527603603"},{"key":"e_1_3_2_1_10_1","unstructured":"Andrea Peruffo Daniele Ahmed and Alessandro Abate. 2021. Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models. In Tools and Algorithms for the Construction and Analysis of Systems. 370--388."},{"key":"e_1_3_2_1_11_1","volume-title":"SOSTOOLS: Sum of squares optimization toolbox for MATLAB","author":"Prajna Stephen","year":"2004","unstructured":"Stephen Prajna. 2004. SOSTOOLS: Sum of squares optimization toolbox for MATLAB. http:\/\/www.mit.edu\/~parrilo\/sostools\/index.html (2004)."},{"key":"e_1_3_2_1_12_1","first-page":"1415","article-title":"A framework for worst-case and stochastic safety verification using barrier certificates","volume":"52","author":"Prajna Stephen","year":"2007","unstructured":"Stephen Prajna, Ali Jadbabaie, and George J. Pappas. 2007. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE TAC 52, 8 (2007), 1415--1429.","journal-title":"IEEE TAC"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Mohamed Amin Ben Sassi and Sriram Sankaranarayanan. 2015. Stabilization of polynomial dynamical systems using linear programming based on Bernstein polynomials. arXiv:1501.04578 [math.OC]","DOI":"10.1145\/2728606.2728639"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586327"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2968478.2968484"}],"event":{"name":"DAC '24: 61st ACM\/IEEE Design Automation Conference","location":"San Francisco CA USA","acronym":"DAC '24","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE-CEDA","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 61st ACM\/IEEE Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649329.3658256","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649329.3658256","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:01Z","timestamp":1750295881000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649329.3658256"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,23]]},"references-count":16,"alternative-id":["10.1145\/3649329.3658256","10.1145\/3649329"],"URL":"https:\/\/doi.org\/10.1145\/3649329.3658256","relation":{},"subject":[],"published":{"date-parts":[[2024,6,23]]},"assertion":[{"value":"2024-11-07","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}