{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T23:17:59Z","timestamp":1768346279935,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,5,19]],"date-time":"2021-05-19T00:00:00Z","timestamp":1621382400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Natural Science Foundation of China","award":["62032010, 61772203, 61772260"],"award-info":[{"award-number":["62032010, 61772203, 61772260"]}]},{"name":"Zhejiang Provincial Natural Science Foundation of China","award":["LY20F020020"],"award-info":[{"award-number":["LY20F020020"]}]},{"name":"Jiangsu Natural Science Foundation","award":["BK20202001"],"award-info":[{"award-number":["BK20202001"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,5,19]]},"DOI":"10.1145\/3447928.3456638","type":"proceedings-article","created":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T03:54:48Z","timestamp":1620100488000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems"],"prefix":"10.1145","author":[{"given":"Qingye","family":"Zhao","sequence":"first","affiliation":[{"name":"University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xin","family":"Chen","sequence":"additional","affiliation":[{"name":"University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yifan","family":"Zhang","sequence":"additional","affiliation":[{"name":"University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Sha","sequence":"additional","affiliation":[{"name":"University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhengfeng","family":"Yang","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wang","family":"Lin","sequence":"additional","affiliation":[{"name":"Zhejiang Sci-Tech University, Hangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enyi","family":"Tang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiguang","family":"Chen","sequence":"additional","affiliation":[{"name":"Nanjing Foreign Language School, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,5,19]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45351-2_9"},{"key":"e_1_3_2_1_2_1","volume-title":"Convex optimization","author":"Boyd Stephen","unstructured":"Stephen Boyd , Stephen P Boyd , and Lieven Vandenberghe . 2004. Convex optimization . Cambridge university press . Stephen Boyd, Stephen P Boyd, and Lieven Vandenberghe. 2004. Convex optimization. Cambridge university press."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02551274"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2016.07.010"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"e_1_3_2_1_6_1","volume-title":"Automated Technology for Verification and Analysis","author":"Fan Chuchu","unstructured":"Chuchu Fan and Sayan Mitra . 2015. Bounded Verification with On-the-Fly Discrepancy Computation . In Automated Technology for Verification and Analysis , Bernd Finkbeiner , Geguang Pu, and Lijun Zhang (Eds.). Springer International Publishing , Cham, 446--463. Chuchu Fan and Sayan Mitra. 2015. Bounded Verification with On-the-Fly Discrepancy Computation. In Automated Technology for Verification and Analysis, Bernd Finkbeiner, Geguang Pu, and Lijun Zhang (Eds.). Springer International Publishing, Cham, 446--463."},{"key":"e_1_3_2_1_7_1","unstructured":"Sicun Gao. [n.d.]. Quadcopter Model. ([n. d.]). https:\/\/github.com\/dreal\/benchmarks\/blob\/master\/inv\/quadcopter_nonlinear.inv.  Sicun Gao. [n.d.]. Quadcopter Model. ([n. d.]). https:\/\/github.com\/dreal\/benchmarks\/blob\/master\/inv\/quadcopter_nonlinear.inv."},{"key":"e_1_3_2_1_8_1","volume-title":"Deep learning","author":"Goodfellow Ian","unstructured":"Ian Goodfellow , Yoshua Bengio , Aaron Courville , and Yoshua Bengio . 2016. Deep learning . Vol. 1 . MIT press Cambridge . Ian Goodfellow, Yoshua Bengio, Aaron Courville, and Yoshua Bengio. 2016. Deep learning. Vol. 1. MIT press Cambridge."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2014.6859330"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"e_1_3_2_1_11_1","volume-title":"Gurobi optimizer reference manual. URL https:\/\/www.gurobi.com","author":"Optimization Incorporate Gurobi","year":"2020","unstructured":"Incorporate Gurobi Optimization . 2020. Gurobi optimizer reference manual. URL https:\/\/www.gurobi.com ( 2020 ). Incorporate Gurobi Optimization. 2020. Gurobi optimizer reference manual. URL https:\/\/www.gurobi.com (2020)."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0893-6080(89)90020-8"},{"key":"e_1_3_2_1_13_1","volume-title":"Interdisciplinary Topics in Applied Mathematics, Modeling and Computational Science","author":"Kapinski James","unstructured":"James Kapinski and Jyotirmoy Deshmukh . 2015. Discovering forward invariant sets for nonlinear dynamical systems . In Interdisciplinary Topics in Applied Mathematics, Modeling and Computational Science . Springer , 259--264. James Kapinski and Jyotirmoy Deshmukh. 2015. Discovering forward invariant sets for nonlinear dynamical systems. In Interdisciplinary Topics in Applied Mathematics, Modeling and Computational Science. Springer, 259--264."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562139"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_2_1_16_1","volume-title":"Applications of interval computations","author":"Baker Kearfott R","unstructured":"R Baker Kearfott and Vladik Kreinovich . 2013. Applications of interval computations . Vol. 3 . Springer Science & Business Media . R Baker Kearfott and Vladik Kreinovich. 2013. Applications of interval computations. Vol. 3. Springer Science & Business Media."},{"key":"e_1_3_2_1_17_1","volume-title":"Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980","author":"Kingma Diederik P","year":"2014","unstructured":"Diederik P Kingma and Jimmy Ba . 2014 . Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014). Diederik P Kingma and Jimmy Ba. 2014. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014)."},{"key":"e_1_3_2_1_18_1","volume-title":"Systems Biology in Practice: Concepts, Implementation and Application","author":"Klipp Edda","unstructured":"Edda Klipp , Ralf Herwig , Axel Kowald , Christoph Wierling , and Hans Lehrach . 2005. Systems Biology in Practice: Concepts, Implementation and Application . Wiley-Blackwell . Edda Klipp, Ralf Herwig, Axel Kowald, Christoph Wierling, and Hans Lehrach. 2005. Systems Biology in Practice: Concepts, Implementation and Application. Wiley-Blackwell."},{"key":"e_1_3_2_1_19_1","volume-title":"PENBMI user's guide. Avaiable from http:\/\/www.penopt.com","author":"Kocvara Michal","year":"2005","unstructured":"Michal Kocvara and Michael Stingl . 2005. PENBMI user's guide. Avaiable from http:\/\/www.penopt.com ( 2005 ). Michal Kocvara and Michael Stingl. 2005. PENBMI user's guide. Avaiable from http:\/\/www.penopt.com (2005)."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_17"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxt059"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038659"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_23"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70139-4"},{"key":"e_1_3_2_1_25_1","volume-title":"Arnaldo Vieira Moura, and Rachid Rebiha","author":"Matringe Nadir","year":"2010","unstructured":"Nadir Matringe , Arnaldo Vieira Moura, and Rachid Rebiha . 2010 . Generating invariants for non-linear hybrid systems by linear algebraic methods. In Proc. of the Static Analysis. Springer , 373--389. Nadir Matringe, Arnaldo Vieira Moura, and Rachid Rebiha. 2010. Generating invariants for non-linear hybrid systems by linear algebraic methods. In Proc. of the Static Analysis. Springer, 373--389."},{"key":"e_1_3_2_1_26_1","volume-title":"Automated Formal Synthesis of Neural Barrier Certificates for Dynamical Models. arXiv preprint arXiv:2007.03251","author":"Peruffo Andrea","year":"2020","unstructured":"Andrea Peruffo , Daniele Ahmed , and Alessandro Abate . 2020. Automated Formal Synthesis of Neural Barrier Certificates for Dynamical Models. arXiv preprint arXiv:2007.03251 ( 2020 ). Andrea Peruffo, Daniele Ahmed, and Alessandro Abate. 2020. Automated Formal Synthesis of Neural Barrier Certificates for Dynamical Models. arXiv preprint arXiv:2007.03251 (2020)."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0079-8"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.902736"},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the 34th International Conference on Machine Learning, ICML 2017","author":"Raghu Maithra","year":"2017","unstructured":"Maithra Raghu , Ben Poole , Jon M. Kleinberg , Surya Ganguli , and Jascha Sohl-Dickstein . 2017 . On the Expressive Power of Deep Neural Networks . In Proceedings of the 34th International Conference on Machine Learning, ICML 2017 , Sydney, NSW, Australia, 6- -11 August 2017. 2847--2854. Maithra Raghu, Ben Poole, Jon M. Kleinberg, Surya Ganguli, and Jascha Sohl-Dickstein. 2017. On the Expressive Power of Deep Neural Networks. In Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6--11 August 2017. 2847--2854."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_38"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755952.1755984"},{"key":"e_1_3_2_1_33_1","volume-title":"Reachability Analysis Using Message Passing over Tree Decompositions","author":"Sankaranarayanan Sriram","unstructured":"Sriram Sankaranarayanan . 2020. Reachability Analysis Using Message Passing over Tree Decompositions . In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing , Cham , 604--628. Sriram Sankaranarayanan. 2020. Reachability Analysis Using Message Passing over Tree Decompositions. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham, 604--628."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0046-1"},{"key":"e_1_3_2_1_35_1","unstructured":"Gagandeep Singh Timon Gehr Matthew Mirman Markus P\u00fcschel and Martin Vechev. 2018. Fast and effective robustness certification. In Advances in Neural Information Processing Systems. 10802--10813.  Gagandeep Singh Timon Gehr Matthew Mirman Markus P\u00fcschel and Martin Vechev. 2018. Fast and effective robustness certification. In Advances in Neural Information Processing Systems. 10802--10813."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185632.2185639"},{"key":"e_1_3_2_1_38_1","unstructured":"Jasper Snoek Hugo Larochelle and Ryan P Adams. 2012. Practical bayesian optimization of machine learning algorithms. In Advances in neural information processing systems. 2951--2959.  Jasper Snoek Hugo Larochelle and Ryan P Adams. 2012. Practical bayesian optimization of machine learning algorithms. In Advances in neural information processing systems. 2951--2959."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_13"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993886.1993935"},{"key":"e_1_3_2_1_41_1","volume-title":"Verifying neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356","author":"Tjeng Vincent","year":"2017","unstructured":"Vincent Tjeng and Russ Tedrake . 2017. Verifying neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356 ( 2017 ), 945--950. Vincent Tjeng and Russ Tedrake. 2017. Verifying neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356 (2017), 945--950."},{"key":"e_1_3_2_1_42_1","volume-title":"Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356","author":"Tjeng Vincent","year":"2017","unstructured":"Vincent Tjeng , Kai Xiao , and Russ Tedrake . 2017. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356 ( 2017 ). Vincent Tjeng, Kai Xiao, and Russ Tedrake. 2017. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356 (2017)."},{"key":"e_1_3_2_1_43_1","volume-title":"Proceedings of the 55th Annual Design Automation Conference, DAC 2018","author":"Tuncali Cumhur Erkan","year":"2018","unstructured":"Cumhur Erkan Tuncali , James Kapinski , Hisahiro Ito , and Jyotirmoy V. Deshmukh . 2018. Reasoning about safety of learning-enabled components in autonomous cyber-physical systems . In Proceedings of the 55th Annual Design Automation Conference, DAC 2018 , San Francisco, CA, USA, June 24--29 , 2018 . ACM, 30:1--30:6. Cumhur Erkan Tuncali, James Kapinski, Hisahiro Ito, and Jyotirmoy V. Deshmukh. 2018. Reasoning about safety of learning-enabled components in autonomous cyber-physical systems. In Proceedings of the 55th Annual Design Automation Conference, DAC 2018, San Francisco, CA, USA, June 24--29, 2018. ACM, 30:1--30:6."},{"key":"e_1_3_2_1_44_1","volume-title":"27th {USENIX} Security Symposium ({USENIX} Security 18). 1599--1614.","author":"Wang Shiqi","unstructured":"Shiqi Wang , Kexin Pei , Justin Whitehouse , Junfeng Yang , and Suman Jana . 2018. Formal security analysis of neural networks using symbolic intervals . In 27th {USENIX} Security Symposium ({USENIX} Security 18). 1599--1614. Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal security analysis of neural networks using symbolic intervals. In 27th {USENIX} Security Symposium ({USENIX} Security 18). 1599--1614."},{"key":"e_1_3_2_1_45_1","volume-title":"isat3. URL https:\/\/projects.informatik.unifreiburg.de\/projects\/isat3","author":"Winterer Felix","year":"2017","unstructured":"Felix Winterer . 2017. isat3. URL https:\/\/projects.informatik.unifreiburg.de\/projects\/isat3 ( 2017 ). Felix Winterer. 2017. isat3. URL https:\/\/projects.informatik.unifreiburg.de\/projects\/isat3 (2017)."},{"key":"e_1_3_2_1_46_1","volume-title":"International Conference on Machine Learning. PMLR, 5286--5295","author":"Wong Eric","year":"2018","unstructured":"Eric Wong and Zico Kolter . 2018 . Provable defenses against adversarial examples via the convex outer adversarial polytope . In International Conference on Machine Learning. PMLR, 5286--5295 . Eric Wong and Zico Kolter. 2018. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning. PMLR, 5286--5295."},{"key":"e_1_3_2_1_47_1","volume-title":"Probably Approximate Safety Verification of Hybrid Dynamical Systems. In International Conference on Formal Engineering Methods. Springer, 236--252","author":"Xue Bai","year":"2019","unstructured":"Bai Xue , Martin Fr\u00e4nzle , Hengjun Zhao , Naijun Zhan , and Arvind Easwaran . 2019 . Probably Approximate Safety Verification of Hybrid Dynamical Systems. In International Conference on Formal Engineering Methods. Springer, 236--252 . Bai Xue, Martin Fr\u00e4nzle, Hengjun Zhao, Naijun Zhan, and Arvind Easwaran. 2019. Probably Approximate Safety Verification of Hybrid Dynamical Systems. In International Conference on Formal Engineering Methods. Springer, 236--252."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629424"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2019.100837"},{"key":"e_1_3_2_1_50_1","volume-title":"Proc. of 2016 International Conference on Embedded Software, EMSOFT 2016","author":"Zeng Xia","year":"2016","unstructured":"Xia Zeng , Wang Lin , Zhengfeng Yang , Xin Chen , and Lilei Wang . 2016 . Darbouxtype barrier certificates for safety verification of nonlinear hybrid systems . In Proc. of 2016 International Conference on Embedded Software, EMSOFT 2016 , Pittsburgh, Pennsylvania, USA, October 1--7 , 2016, Petru Eles and Rahul Mangharam (Eds.). ACM, 11:1--11:10. Xia Zeng, Wang Lin, Zhengfeng Yang, Xin Chen, and Lilei Wang. 2016. Darbouxtype barrier certificates for safety verification of nonlinear hybrid systems. In Proc. of 2016 International Conference on Embedded Software, EMSOFT 2016, Pittsburgh, Pennsylvania, USA, October 1--7, 2016, Petru Eles and Rahul Mangharam (Eds.). ACM, 11:1--11:10."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382222"}],"event":{"name":"HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control","location":"Nashville Tennessee","acronym":"HSCC '21","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3447928.3456638","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3447928.3456638","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:23Z","timestamp":1750195703000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3447928.3456638"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,19]]},"references-count":51,"alternative-id":["10.1145\/3447928.3456638","10.1145\/3447928"],"URL":"https:\/\/doi.org\/10.1145\/3447928.3456638","relation":{},"subject":[],"published":{"date-parts":[[2021,5,19]]},"assertion":[{"value":"2021-05-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}