{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:27:46Z","timestamp":1778498866144,"version":"3.51.4"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720155","type":"print"},{"value":"9783030720162","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The approach is underpinned by an inductive framework: this is structured as a sequential loop between a learner, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate\u2019s validity or generates counter-examples to further guide the learner. We compare the approach against state-of-the-art techniques, over polynomial and non-polynomial dynamical models: the outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine (up to three orders less), whilst needing a far smaller data set (up to three orders less) for the learning part. Beyond improvements over the state of the art, we further challenge the new approach on a hybrid dynamical model and on larger-dimensional models, and showcase the numerical robustness of our algorithms and codebase.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_20","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"370-388","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":37,"title":["Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7767-2935","authenticated-orcid":false,"given":"Andrea","family":"Peruffo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5479-741X","authenticated-orcid":false,"given":"Daniele","family":"Ahmed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-9093","authenticated-orcid":false,"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe, and Andrea Peruffo. FOSSIL: A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates using Neural Networks.In HSCC. ACM, 2021.","DOI":"10.1109\/LCSYS.2020.3005328"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. Formal Synthesis of Lyapunov Neural Networks. IEEE Control Systems Letters, 5(3):773\u2013778, 2021.","DOI":"10.1109\/LCSYS.2020.3005328"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, and Elizabeth Polgreen. Counterexample Guided Inductive Synthesis Modulo Theories. In Proceedings of CAV, LNCS 10981, pages 270\u2013288, 2018.","DOI":"10.1007\/978-3-319-96145-3_15"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Alessandro Abate, Ashish Tiwari, and Shankar Sastry. Box Invariance in Biologically-inspired Dynamical Systems. Automatica, 45(7):1601\u20131610, 2009.","DOI":"10.1016\/j.automatica.2009.02.028"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Daniele Ahmed, Andrea Peruffo, and Alessandro Abate. Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers. In TACAS (1), volume 12078 of LNCS, pages 97\u2013114. Springer, 2020.","DOI":"10.1007\/978-3-030-45190-5_6"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Andrew\u00a0J Barry, Anirudha Majumdar, and Russ Tedrake. Safety Verification of Reactive Controllers for UAV Flight in Cluttered Environments using Barrier Certificates. In 2012 IEEE International Conference on Robotics and Automation, pages 484\u2013490. IEEE, 2012.","DOI":"10.1109\/ICRA.2012.6225351"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Urs Borrmann, Li\u00a0Wang, Aaron\u00a0D Ames, and Magnus Egerstedt. Control Barrier Certificates for Safe Swarm Behavior. IFAC-PapersOnLine, 48(27):68\u201373, 2015.","DOI":"10.1016\/j.ifacol.2015.11.154"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Dario Cattaruzza, Alessandro Abate, Peter Schrammel, and Daniel Kroening. Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration. Journal of Automated Reasoning, 2020.","DOI":"10.1007\/s10817-020-09562-z"},{"key":"20_CR9","unstructured":"Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov Control. In NeurIPS, pages 3240\u20133249, 2019"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Liyun Dai, Ting Gan, Bican Xia, and Naijun Zhan. Barrier Certificates Revisited. Journal of Symbolic Computation, 80:62\u201386, 2017.","DOI":"10.1016\/j.jsc.2016.07.010"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Leonardo de\u00a0Moura and Nikolaj Bj\u00f8rner.Z3: An Efficient SMT Solver. In TACAS, volume 4963 of LNCS, pages 337\u2013340. Springer, 2008.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Sicun Gao, Jeremy Avigad, and Edmund\u00a0M Clarke. $$\\delta $$-complete Decision Procedures for Satisfiability over the Reals. In International Joint Conference on Automated Reasoning, pages 286\u2013300. Springer, 2012.","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Sicun Gao, Soonho Kong, and Edmund\u00a0M Clarke. dReal: An SMT Solver for Nonlinear Theories over the Reals. In International conference on automated deduction, pages 208\u2013214. Springer, 2013.","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Hui Kong, Fei He, Xiaoyu Song, William\u00a0NN Hung, and Ming Gu. Exponential-condition-based Barrier Certificate Generation for Safety Verification of Hybrid Systems. In International Conference on Computer Aided Verification, pages 242\u2013257. Springer, 2013.","DOI":"10.1007\/978-3-642-39799-8_17"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Daniel Kroening and Ofer Strichman. Decision Procedures - An Algorithmic Point of View.Springer Verlag, 2016.","DOI":"10.1007\/978-3-662-50497-0"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Beno\u00eet Legat, Paulo Tabuada, and Rapha\u00ebl\u00a0M Jungers. Sum-of-Squares Methods for Controlled Invariant Sets with Applications to Model-predictive Control. Nonlinear Analysis: Hybrid Systems, 36:100858, 2020.","DOI":"10.1016\/j.nahs.2020.100858"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Jiang Liu, Naijun Zhan, Hengjun Zhao, and Liang Zou. Abstraction of Elementary Hybrid Systems by Variable Transformation. In International Symposium on Formal Methods, pages 360\u2013377. Springer, 2015.","DOI":"10.1007\/978-3-319-19249-9_23"},{"key":"20_CR18","unstructured":"A.\u00a0Papachristodoulou, J.\u00a0Anderson, G.\u00a0Valmorbida, S.\u00a0Prajna, P.\u00a0Seiler, and P.\u00a0A. Parrilo. SOSTOOLS: Sum of squares optimization toolbox for MATLAB. http:\/\/arxiv.org\/abs\/1310.4716, 2013."},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Andr\u00e9 Platzer and Edmund\u00a0M Clarke. Computing Differential Invariants of Hybrid Systems as Fixedpoints. In International Conference on Computer Aided Verification, pages 176\u2013189. Springer, 2008.","DOI":"10.1007\/978-3-540-70545-1_17"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Stephen Prajna. Barrier Certificates for Nonlinear Model Validation. Automatica, 42(1):117\u2013126, 2006.","DOI":"10.1016\/j.automatica.2005.08.007"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Stephen Prajna and Ali Jadbabaie . Safety Verification of Hybrid Systems Using Barrier Certificates. In International Workshop on Hybrid Systems: Computation and Control, pages 477\u2013492. Springer, 2004.","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Stephen Prajna, Ali Jadbabaie , and George\u00a0J Pappas . A Framework for Worst-case and Stochastic Safety Verification Using Barrier Certificates. IEEE Transactions on Automatic Control, 52(8):1415\u20131428, 2007.","DOI":"10.1109\/TAC.2007.902736"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Hadi Ravanbakhsh and Sriram Sankaranarayanan. Counter-example guided synthesis of control lyapunov functions for switched systems. In IEEE Control and Decision Conference (CDC), pages 4232\u20134239, 2015.","DOI":"10.1109\/CDC.2015.7402879"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Hadi Ravanbakhsh and Sriram Sankaranarayanan. Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework. In ACM\/IEEE Conference on Embedded Software (EMSOFT), pages 8:1\u20138:10, 2016.","DOI":"10.1145\/2968478.2968485"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Hadi Ravanbakhsh and Sriram Sankaranarayanan. Learning Control Lyapunov Functions from Counterexamples and Demonstrations. Autonomous Robots, pages 1\u201333, 2018.","DOI":"10.15607\/RSS.2017.XIII.049"},{"key":"20_CR26","unstructured":"Spencer\u00a0M. Richards, Felix Berkenkamp, and Andreas Krause. The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems. In CoRL, volume\u00a087 of Proceedings of Machine Learning Research, pages 466\u2013476. PMLR, 2018."},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Sriram Sankaranarayanan, Xin Chen, and Erika Abraham. Lyapunov Function Synthesis using Handelman Representations. IFAC Proceedings Volumes, 46(23):576\u2013581, 2013.","DOI":"10.3182\/20130904-3-FR-2041.00198"},{"key":"20_CR28","unstructured":"Shankar Sastry. Nonlinear Systems: Analysis, Stability and Control.Springer Verlag, 1999."},{"key":"20_CR29","unstructured":"Christoffer Sloth, George\u00a0J Pappas, and Rafael Wisniewski. Compositional Safety Analysis using Barrier Certificates. In Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, pages 15\u201324, 2012."},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Andrew Sogokon, Khalil Ghorbal, Yong\u00a0Kiam Tan, and Andr\u00e9 Platzer. Vector Barrier Certificates and Comparison Systems. In International Symposium on Formal Methods, pages 418\u2013437. Springer, 2018.","DOI":"10.1007\/978-3-319-95582-7_25"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. In Proceedings of the 12th international conference on Architectural support for programming languages and operating systems, pages 404\u2013415, 2006.","DOI":"10.1145\/1168857.1168907"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"Li\u00a0Wang, Aaron\u00a0D Ames, and Magnus Egerstedt. Safety Barrier Certificates for Collisions-free Multirobot Systems. IEEE Transactions on Robotics, 33(3):661\u2013674, 2017","DOI":"10.1109\/TRO.2017.2659727"},{"key":"20_CR33","doi-asserted-by":"crossref","unstructured":"Xia Zeng, Wang Lin, Zhengfeng Yang, Xin Chen, and Lilei Wang. Darboux-type Barrier Certificates for Safety Verification of Nonlinear Hybrid Systems. In Proceedings of the 13th International Conference on Embedded Software, pages 1\u201310, 2016.","DOI":"10.1145\/2968478.2968484"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Hengjun Zhao, Xia Zeng, Taolue Chen, and Zhiming Liu. Synthesizing Barrier Certificates Using Neural Networks. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, HSCC \u201920, New York, NY, USA, 2020. Association for Computing Machinery.","DOI":"10.1145\/3365365.3382222"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T00:09:33Z","timestamp":1616371773000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}