{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:30:34Z","timestamp":1773808234736,"version":"3.50.1"},"reference-count":0,"publisher":"Association for the Advancement of Artificial Intelligence (AAAI)","issue":"42","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAAI"],"abstract":"<jats:p>Barrier certificates play an important role in verifying the safety of continuous-time systems, including autonomous driving, robotic manipulators and other critical applications. Recently, \nReLU neural barrier certificates---barrier certificates represented by the ReLU neural networks---have attracted significant attention in the safe control community due to their promising performance.\nHowever, because of the approximate nature of neural networks, rigorous verification methods are required to ensure the correctness of these certificates. This paper presents  a necessary and sufficient condition for verifying  the correctness of ReLU\nneural barrier certificates. The proposed condition can be encoded  as either an Satisfiability Modulo Theories (SMT) or  optimization problem, enabling both verification and falsification.  To the best of our knowledge, this is the first approach\ncapable of falsifying ReLU neural barrier certificates. Numerical experiments demonstrate the validity and \neffectiveness of the proposed method in both verifying and falsifying such certificates.<\/jats:p>","DOI":"10.1609\/aaai.v40i42.40890","type":"journal-article","created":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T03:35:31Z","timestamp":1773804931000},"page":"35767-35774","source":"Crossref","is-referenced-by-count":0,"title":["Efficient Verification and Falsification of ReLU Neural Barrier Certificates"],"prefix":"10.1609","volume":"40","author":[{"given":"Dejin","family":"Ren","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yiling","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taoran","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bai","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"9382","published-online":{"date-parts":[[2026,3,14]]},"container-title":["Proceedings of the AAAI Conference on Artificial Intelligence"],"original-title":[],"link":[{"URL":"https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/download\/40890\/44851","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/download\/40890\/44851","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T03:35:33Z","timestamp":1773804933000},"score":1,"resource":{"primary":{"URL":"https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/40890"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,14]]},"references-count":0,"journal-issue":{"issue":"42","published-online":{"date-parts":[[2026,3,17]]}},"URL":"https:\/\/doi.org\/10.1609\/aaai.v40i42.40890","relation":{},"ISSN":["2374-3468","2159-5399"],"issn-type":[{"value":"2374-3468","type":"electronic"},{"value":"2159-5399","type":"print"}],"subject":[],"published":{"date-parts":[[2026,3,14]]}}}