pith. the verified trust layer for science. sign in

arxiv: 2511.06341 · v2 · submitted 2025-11-09 · 💻 cs.LG · cs.RO· cs.SY· eess.SY· math.OC

Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

Nikolaus Vertovec , Frederik Baymler Mathiesen , Thom Badings , Luca Laurenti , Alessandro Abate This is my paper

Pith reviewed 2026-05-17 23:32 UTC · model grok-4.3

classification 💻 cs.LG cs.ROcs.SYeess.SYmath.OC
keywords neural control barrier functionsverificationlinear bound propagationsafety certificationneural networkscontrol-affine systemsMcCormick relaxation
0
0 comments X p. Extension

The pith

Linear bound propagation on network gradients yields scalable checks for neural control barrier functions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The authors develop a verification method for neural networks that serve as control barrier functions, which certify that a dynamical system stays safe under feedback control. They extend linear bound propagation to obtain bounds on the network's gradients and then apply McCormick relaxations to produce linear upper and lower bounds on the CBF conditions themselves. An adaptive, parallelizable refinement step tightens these bounds over selected regions of the state space. If the bounds remain sufficiently tight, the approach certifies validity for networks too large for prior verification tools, broadening the class of dynamics and safety sets that can be handled with expressive neural certificates.

Core claim

We present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF. Our approach is rooted in linear bound propagation for neural networks, which we extend to compute bounds on the gradients of the network. Combined with McCormick relaxation, we derive linear upper and lower bounds on the CBF conditions, thereby eliminating the need for computationally expensive verification procedures. Our approach applies to arbitrary control-affine systems and a broad range of nonlinear activation functions. To reduce conservatism, we develop a parallelizable refinement strategy that adaptively refines the

What carries the argument

Linear bound propagation extended to network gradients, combined with McCormick envelopes to produce linear bounds on the CBF Lie-derivative conditions.

Load-bearing premise

The upper and lower bounds obtained from gradient propagation and McCormick relaxations remain tight enough after adaptive refinement to certify the CBF conditions over the full state space without prohibitive conservatism.

What would settle it

Run the method on a neural CBF known to be valid by an exact but slower verifier; if it reports invalidity, or conversely certifies an invalid network, the claim fails.

Figures

Figures reproduced from arXiv: 2511.06341 by Alessandro Abate, Frederik Baymler Mathiesen, Luca Laurenti, Nikolaus Vertovec, Thom Badings.

Figure 1
Figure 1. Figure 1: Verification flowchart illustrating the refinement and validation procedure for each simplex. Batching simplices Our approach enables efficient utilization of computational resources by performing LBP on batches of simplices using GPUs. In particular, we collect simplices that require evaluation of ψinvar into batches and compute the necessary linear bounds on the invariance condition jointly over each bat… view at source ↗
Figure 2
Figure 2. Figure 2: Illustration of the neural control barrier function Bθ(x), the CBF invariance condition from Eq. (2), and the resulting verification regions after adaptive mesh refinement [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: ReLU Relaxation. For the Rectified Linear Unit σ(y) = max(0, y), the relaxation depends on whether the interval crosses zero. • Active region (l ≥ 0): Gm = Gm = 1, gm = gm = 0. Sm = Sm = 0, sm = sm = 1. • Inactive region (u ≤ 0): Gm = Gm = 0, gm = gm = 0. Sm = Sm = 0, sm = sm = 0. • Unstable region (l < 0 < u): Gm = 0, Gm = u u − l , gm = 0, gm = −l Gm. Sm = Sm = 0, sm = 0, sm = 1, B. Leaky ReLU Relaxation… view at source ↗
Figure 4
Figure 4. Figure 4: Leaky ReLU Relaxation. • Unstable region (l < 0 < u): Gm = α, Gm = u − αl u − l , gm = 0, gm = u − Gm u. Sm = Sm = 0, sm = α, sm = 1, C. Sigmoid Relaxation [PITH_FULL_IMAGE:figures/full_fig_p018_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Sigmoid Relaxation. The sigmoid activation σ(y) = 1 1+e−y is convex for y < 0 and concave for y > 0. The derivative has inflection points at ± log 3+√ 3 3− √ 3 and is concave in between the inflection points, and convex when 18 [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Derivative of Sigmoid Relaxation. the domain lies outside the inflection points. Define mact = σ(u) − σ(l) u − l , mder = σ ′ (u) − σ ′ (l) u − l . Let t⋆ ∈ (0, 1) solve 2t 3 − 3t 2 + t − mder = 0 and define x⋆ = log t⋆ 1−t⋆ ∈ (l, u). Then • Convex region: Gm = σ ′ (u), Gm = mact, gm = σ(u) − σ ′ (u) u, gm = σ(l) − mact l, Sm = mder, Sm = mder, sm = σ ′ (x⋆) − mder x⋆, sm = σ ′ (u) − mder u. • Concave regi… view at source ↗
Figure 7
Figure 7. Figure 7: Tanh Relaxation [PITH_FULL_IMAGE:figures/full_fig_p020_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Derivative Tanh Relaxation. The hyperbolic tangent activation σ(y) = tanh(y) is convex for y < 0 and concave for y > 0. The derivative has inflection points at ± arctanh √ 1 3 and is concave in between the inflection points, and convex when the domain lies outside the inflection points. 20 [PITH_FULL_IMAGE:figures/full_fig_p020_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: 2D-Control: Illustration of the barrier function Bθ(x), the CBF invariance condition, and the resulting verification regions after adaptive mesh refinement. States x = (x1, x2) ∈ R 2 with affine control u = (u1, u2) and dynamics: x˙ =  −x1x2 −x 2 2  +  1 0 0 1 u, (35) Control bounds are u ∈ [− 1 2 , 1 2 ] 2 . The state space is X = [−3, 3] × [−2, 2], with the safe set defined as S = X \{(x, y) ∈ R 2 | … view at source ↗
Figure 10
Figure 10. Figure 10: Darboux: Illustration of the barrier function Bθ(x), the CBF invariance condition, and the resulting verification regions after adaptive mesh refinement. Originally presented in Zeng et al. (2016), the system has been reported to not admit an LMI￾based barrier function with a degree less than 6 (Abate et al., 2021a), making it a common benchmark to demonstrate the expressivity of neural CBFs. Using a larg… view at source ↗
Figure 11
Figure 11. Figure 11: Barrier 2: Illustration of the barrier function Bθ(x), the CBF invariance condition, and the resulting verification regions after adaptive mesh refinement. Presented in Liu et al. (2015) and chosen for its high degree of nonlinearity and non-polynomial (exponential and trigonometric) terms. States x = (x1, x2) ∈ R 2 and autonomous dynamics: x˙1 = " e −x1 + x2 − 1 − sin2 (x1) # , (42) The state space is X … view at source ↗
Figure 12
Figure 12. Figure 12: Barrier 3: Illustration of the barrier function Bθ(x), the CBF invariance condition, and the resulting verification regions after adaptive mesh refinement. A modification of the dynamical system presented in Prajna (2006) with non-convex domains, as in Abate et al. (2021a). States x = (x1, x2) ∈ R 2 and autonomous dynamics: x˙ =  x2 −x1 − x2 + 1 3 x 3 1  . (43) The state space is X = [−3, 2.5] × [−2, 1]… view at source ↗
read the original abstract

Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems. Recently, CBFs represented as neural networks have shown great promise due to their expressiveness and applicability to a broad class of dynamics and safety constraints. However, verifying that a trained neural network is indeed a valid CBF is a computational bottleneck that limits the size of the networks that can be used. To overcome this limitation, we present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF. Our approach is rooted in linear bound propagation (LBP) for neural networks, which we extend to compute bounds on the gradients of the network. Combined with McCormick relaxation, we derive linear upper and lower bounds on the CBF conditions, thereby eliminating the need for computationally expensive verification procedures. Our approach applies to arbitrary control-affine systems and a broad range of nonlinear activation functions. To reduce conservatism, we develop a parallelizable refinement strategy that adaptively refines the regions over which these bounds are computed. Our approach scales to larger neural networks than state-of-the-art verification procedures for CBFs, as demonstrated by our numerical experiments.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The paper introduces a verification framework for neural network control barrier functions (CBFs) on control-affine systems. It extends linear bound propagation (LBP) to obtain linear upper/lower bounds on both the network output and its gradient, then applies McCormick relaxations to the bilinear terms appearing in the Lie-derivative CBF condition. An adaptive, parallelizable partitioning scheme is used to tighten the bounds until the certified lower bound on sup_u (L_f h + L_g h u) + α(h) is non-negative over the entire domain. The central claim is that this procedure scales to larger networks than existing SMT-based or optimization-based CBF verifiers, as demonstrated by numerical experiments.

Significance. If the tightness and scalability claims hold, the method would remove a major computational obstacle to deploying expressive neural CBFs on higher-dimensional or more complex control-affine plants. The combination of established LBP primitives with McCormick envelopes and adaptive refinement is a natural and potentially practical advance over purely symbolic or SMT approaches. The numerical experiments provide initial evidence that the approach can handle networks larger than those verified by prior art.

major comments (3)
  1. [§4.2] §4.2 and Algorithm 1: the adaptive refinement procedure is described at a high level, but no explicit bound is given on the worst-case number of regions or the depth of the refinement tree as a function of state dimension or network width. Without such an analysis or a worst-case example, it is difficult to assess whether the claimed scalability advantage over SMT solvers persists when the McCormick envelopes or gradient bounds become loose.
  2. [§3.3] §3.3, Eq. (12)–(15): the McCormick relaxation is applied to the product L_g h(x)·u. The manuscript should state the precise interval bounds used for u and for the gradient components, and should quantify how the relaxation gap grows with the width of those intervals. If the intervals are not tightened during refinement, the certified lower bound may remain negative even when a valid CBF exists.
  3. [Experiments] Experiments section, Table 2: the reported verification times and network sizes are compared only against a single baseline (SMT-based verifier). A more informative comparison would include at least one additional relaxation-based or abstraction-refinement method to isolate the contribution of the LBP+McCormick combination.
minor comments (2)
  1. [§2] Notation for the control-affine dynamics f(x) and g(x) is introduced without an explicit statement of the assumed regularity (e.g., Lipschitz constants or boundedness of g).
  2. [Figure 3] Figure 3 caption should clarify whether the plotted lower bounds are the final certified values after refinement or intermediate values.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for their constructive and detailed comments on our manuscript. We have addressed each major comment below, making revisions where appropriate to improve clarity and completeness while maintaining the core contributions.

read point-by-point responses

  1. Referee: [§4.2] §4.2 and Algorithm 1: the adaptive refinement procedure is described at a high level, but no explicit bound is given on the worst-case number of regions or the depth of the refinement tree as a function of state dimension or network width. Without such an analysis or a worst-case example, it is difficult to assess whether the claimed scalability advantage over SMT solvers persists when the McCormick envelopes or gradient bounds become loose.

    Authors: We agree that a formal worst-case analysis of the refinement tree would strengthen the presentation. Deriving a tight, general bound is challenging because the number of partitions depends on the initial bound tightness, the specific dynamics, and the network weights rather than solely on dimension or width. In the worst case the tree depth can grow exponentially with state dimension, similar to other adaptive abstraction-refinement schemes. We have added a new paragraph to Section 4.2 that explicitly states this limitation, provides a simple worst-case example on a one-dimensional system, and explains why the parallelizable adaptive stopping criterion still yields practical scalability on the networks tested in the experiments. revision: partial

  2. Referee: [§3.3] §3.3, Eq. (12)–(15): the McCormick relaxation is applied to the product L_g h(x)·u. The manuscript should state the precise interval bounds used for u and for the gradient components, and should quantify how the relaxation gap grows with the width of those intervals. If the intervals are not tightened during refinement, the certified lower bound may remain negative even when a valid CBF exists.

    Authors: We thank the referee for highlighting this point. In the revised Section 3.3 we now explicitly state that the control set U is taken to be a compact hyper-rectangle (e.g., U = [-1,1]^m in all reported experiments) and that the interval bounds on each component of L_g h(x) are those returned by the extended linear bound propagation procedure over the current partition region. We have also added a short derivation showing that the McCormick relaxation gap for the bilinear term is bounded by (1/4)·w_a·w_b, where w_a and w_b are the widths of the intervals for L_g h and u, respectively. Because refinement partitions the state domain, the LBP-computed gradient bounds tighten monotonically, thereby reducing the gap; this dependence is now quantified in the text. revision: yes

  3. Referee: Experiments section, Table 2: the reported verification times and network sizes are compared only against a single baseline (SMT-based verifier). A more informative comparison would include at least one additional relaxation-based or abstraction-refinement method to isolate the contribution of the LBP+McCormick combination.

    Authors: We acknowledge that a single baseline limits the ability to isolate the benefit of the LBP+McCormick combination. In the revised experiments section we have added two further baselines: (i) a pure interval-arithmetic + McCormick verifier without linear bound propagation on gradients, and (ii) a uniform-grid abstraction-refinement method. The updated Table 2 now reports verification times and success rates for all three methods on the same network suite, thereby highlighting the contribution of the gradient bounds obtained via LBP. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation uses established external primitives

full rationale

The paper's core derivation extends linear bound propagation (LBP) to neural network gradients and combines it with McCormick envelopes on the bilinear terms arising in the Lie derivative of the neural CBF. These primitives are drawn from the independent literature on neural verification and convex relaxations rather than being defined in terms of the target CBF conditions or fitted to them. The adaptive partitioning step is a standard refinement heuristic to tighten bounds and does not presuppose the final certified result. No equation reduces by construction to a fitted parameter or to a self-citation whose validity depends on the present work; the method remains self-contained against external benchmarks for bound propagation.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The framework rests on standard domain assumptions from control theory and neural-network verification; no free parameters or new invented entities are introduced in the abstract.

axioms (2)
  • domain assumption The dynamical system is control-affine
    Explicitly stated as the class of systems to which the method applies.
  • domain assumption The activation functions belong to a broad but fixed class for which LBP bounds exist
    Required for the linear bound propagation step to be well-defined.

pith-pipeline@v0.9.0 · 5536 in / 1197 out tokens · 29435 ms · 2026-05-17T23:32:17.698863+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations

    cs.LG 2026-05 unverdicted novelty 6.0

    LightCROWN computes tighter Jacobian bounds for neural networks with smooth nonlinear activations by exploiting their analytical properties, raising verification success rates for neural control barrier functions up t...

Reference graph

Works this paper leans on

42 extracted references · 42 canonical work pages · cited by 1 Pith paper

  1. [1]

    Counterexample guided inductive synthesis modulo theories

    Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, and Elizabeth Polgreen. Counterexample guided inductive synthesis modulo theories. In CAV (1) , volume 10981 of Lecture Notes in Computer Science, pages 270--288. Springer, 2018. doi:10.1007/978-3-319-96145-3_15

    work page doi:10.1007/978-3-319-96145-3_15 2018

  2. [2]

    FOSSIL: a software tool for the formal synthesis of L yapunov functions and barrier certificates using neural networks

    Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe, and Andrea Peruffo. FOSSIL: a software tool for the formal synthesis of L yapunov functions and barrier certificates using neural networks. In HSCC , pages 24:1--24:11. ACM , 2021 a . doi:10.1145/3447928.3456646

    work page doi:10.1145/3447928.3456646 2021

  3. [3]

    Formal synthesis of lyapunov neural networks

    Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. Formal synthesis of lyapunov neural networks. IEEE Control. Syst. Lett. , 5 0 (3): 0 773--778, 2021 b . doi:10.1109/LCSYS.2020.3005328

    work page doi:10.1109/lcsys.2020.3005328 2021

  4. [4]

    Discrete control barrier functions for safety-critical control of discrete systems with application to bipedal robot navigation

    Ayush Agrawal and Koushil Sreenath. Discrete control barrier functions for safety-critical control of discrete systems with application to bipedal robot navigation. In Robotics: Science and Systems, 2017. doi:10.15607/RSS.2017.XIII.073

    work page doi:10.15607/rss.2017.xiii.073 2017

  5. [5]

    Ames, Jessy W

    Aaron D. Ames, Jessy W. Grizzle, and Paulo Tabuada. Control barrier function based quadratic programs with application to adaptive cruise control. In CDC , pages 6271--6278. IEEE , 2014. doi:10.1109/CDC.2014.7040372

    work page doi:10.1109/cdc.2014.7040372 2014

  6. [6]

    Ames, Xiangru Xu, Jessy W

    Aaron D. Ames, Xiangru Xu, Jessy W. Grizzle, and Paulo Tabuada. Control barrier function based quadratic programs for safety critical systems. IEEE Trans. Autom. Control. , 62 0 (8): 0 3861--3876, 2017. doi:10.1109/TAC.2016.2638961

    work page doi:10.1109/tac.2016.2638961 2017

  7. [7]

    Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada

    Aaron D. Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada. Control barrier functions: Theory and applications. In ECC , pages 3420--3431. IEEE , 2019. doi:10.23919/ECC.2019.8796030

    work page doi:10.23919/ecc.2019.8796030 2019

  8. [8]

    Policy verification in stochastic dynamical systems using logarithmic neural certificates

    Thom Badings, Wietze Koops, Sebastian Junges, and Nils Jansen. Policy verification in stochastic dynamical systems using logarithmic neural certificates. In CAV (2) , volume 15932 of Lecture Notes in Computer Science, pages 349--375. Springer, 2025. doi:10.1007/978-3-031-98679-6_16

    work page doi:10.1007/978-3-031-98679-6_16 2025

  9. [9]

    Barry, Anirudha Majumdar, and Russ Tedrake

    Andrew J. Barry, Anirudha Majumdar, and Russ Tedrake. Safety verification of reactive controllers for UAV flight in cluttered environments using barrier certificates. In ICRA , pages 484--490. IEEE , 2012. doi:10.1109/ICRA.2012.6225351

    work page doi:10.1109/icra.2012.6225351 2012

  10. [10]

    Robust control barrier functions under high relative degree and input constraints for satellite trajectories

    Joseph Breeden and Dimitra Panagou. Robust control barrier functions under high relative degree and input constraints for satellite trajectories. Autom., 155: 0 111109, 2023. doi:10.1016/J.AUTOMATICA.2023.111109

    work page doi:10.1016/j.automatica.2023.111109 2023

  11. [11]

    In: 60th IEEE Conference on Decision and Control, pp

    Andrew Clark. Verification and synthesis of control barrier functions. In CDC , pages 6105--6112. IEEE , 2021. doi:10.1109/CDC45484.2021.9683520

    work page doi:10.1109/cdc45484.2021.9683520 2021

  12. [12]

    Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith

    Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM , 50 0 (5): 0 752--794, 2003. doi:10.1145/876638.876643

    work page doi:10.1145/876638.876643 2003

  13. [13]

    Discrete differential geometry: An applied introduction

    Keenan Crane. Discrete differential geometry: An applied introduction. Notices of the AMS, Communication, 1153, 2018

    work page 2018

  14. [14]

    Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control

    Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control. IEEE Trans. Robotics , 39 0 (3): 0 1749--1767, 2023. doi:10.1109/TRO.2022.3232542

    work page doi:10.1109/tro.2022.3232542 2023

  15. [15]

    Automatic abstraction refinement for timed automata

    Henning Dierks, Sebastian Kupferschmid, and Kim Guldstrand Larsen. Automatic abstraction refinement for timed automata. In FORMATS , volume 4763 of Lecture Notes in Computer Science, pages 114--129. Springer, 2007. doi:10.1007/978-3-540-75454-1_10

    work page doi:10.1007/978-3-540-75454-1_10 2007

  16. [16]

    Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models

    Alec Edwards, Andrea Peruffo, and Alessandro Abate. Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models. In HSCC , pages 26:1--26:10. ACM , 2024. doi:10.1145/3641513.3651398

    work page doi:10.1145/3641513.3651398 2024

  17. [17]

    Pawan Kumar

    Francisco Eiras, Adel Bibi, Rudy Bunel, Krishnamurthy Dj Dvijotham, Philip Torr, and M. Pawan Kumar. Efficient error certification for physics-informed neural networks. In ICML . OpenReview.net, 2024

    work page 2024

  18. [18]

    Sicun Gao, Soonho Kong, and Edmund M. Clarke. dreal: An SMT solver for nonlinear theories over the reals. In CADE , volume 7898 of Lecture Notes in Computer Science, pages 208--214. Springer, 2013. doi:10.1007/978-3-642-38574-2_14

    work page doi:10.1007/978-3-642-38574-2_14 2013

  19. [19]

    Kai - Chieh Hsu, Haimin Hu, and Jaime F. Fisac. The safety filter: A unified view of safety-critical control in autonomous systems. Annu. Rev. Control. Robotics Auton. Syst., 7 0 (1), 2024. doi:10.1146/ANNUREV-CONTROL-071723-102940

    work page doi:10.1146/annurev-control-071723-102940 2024

  20. [20]

    Verification of neural control barrier functions with symbolic derivative bounds propagation

    Hanjiang Hu, Yujie Yang, Tianhao Wei, and Changliu Liu. Verification of neural control barrier functions with symbolic derivative bounds propagation. In CoRL, volume 270 of Proceedings of Machine Learning Research, pages 1797--1814. PMLR , 2024

    work page 2024

  21. [21]

    Parameter synthesis for markov models: covering the parameter space

    Sebastian Junges, Erika \' A brah \' a m, Christian Hensel, Nils Jansen, Joost - Pieter Katoen, Tim Quatmann, and Matthias Volk. Parameter synthesis for markov models: covering the parameter space. Formal Methods Syst. Des., 62 0 (1): 0 181--259, 2024. doi:10.1007/S10703-023-00442-X

    work page doi:10.1007/s10703-023-00442-x 2024

  22. [22]

    Kimura and S

    H. Kimura and S. Kobayashi. Stochastic real-valued reinforcement learning to solve a nonlinear control problem. In IEEE SMC'99 Conference Proceedings. 1999 IEEE International Conference on Systems, Man, and Cybernetics (Cat. No.99CH37028), volume 5, pages 510--515 vol.5, 1999. doi:10.1109/ICSMC.1999.815604

    work page doi:10.1109/icsmc.1999.815604 1999

  23. [23]

    Abstraction of elementary hybrid systems by variable transformation

    Jiang Liu, Naijun Zhan, Hengjun Zhao, and Liang Zou. Abstraction of elementary hybrid systems by variable transformation. In FM , volume 9109 of Lecture Notes in Computer Science, pages 360--377. Springer, 2015. doi:10.1007/978-3-319-19249-9_23

    work page doi:10.1007/978-3-319-19249-9_23 2015

  24. [24]

    Calvert, and Luca Laurenti

    Frederik Baymler Mathiesen, Simeon C. Calvert, and Luca Laurenti. Safety certification for stochastic systems via neural barrier functions. IEEE Control. Syst. Lett. , 7: 0 973--978, 2023. doi:10.1109/LCSYS.2022.3229865

    work page doi:10.1109/lcsys.2022.3229865 2023

  25. [25]

    Certified neural approximations of nonlinear dynamics

    Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano, Luca Laurenti, and Alessandro Abate. Certified neural approximations of nonlinear dynamics. CoRR, abs/2505.15497, 2025. doi:10.48550/ARXIV.2505.15497

    work page doi:10.48550/arxiv.2505.15497 2025

  26. [26]

    McCormick

    Garth P. McCormick. Computability of global solutions to factorable nonconvex programs: Part I - convex underestimating problems. Math. Program., 10 0 (1): 0 147--175, 1976. doi:10.1007/BF01580665

    work page doi:10.1007/bf01580665 1976

  27. [27]

    Automated and formal synthesis of neural barrier certificates for dynamical models

    Andrea Peruffo, Daniele Ahmed, and Alessandro Abate. Automated and formal synthesis of neural barrier certificates for dynamical models. In TACAS (1) , volume 12651 of Lecture Notes in Computer Science, pages 370--388. Springer, 2021. doi:10.1007/978-3-030-72016-2_20

    work page doi:10.1007/978-3-030-72016-2_20 2021

  28. [28]

    Barrier certificates for nonlinear model validation

    Stephen Prajna. Barrier certificates for nonlinear model validation. Autom., 42 0 (1): 0 117--126, 2006. doi:10.1016/J.AUTOMATICA.2005.08.007

    work page doi:10.1016/j.automatica.2005.08.007 2006

  29. [29]

    Synthesizing barrier certificates of neural network controlled continuous systems via approximations

    Meng Sha, Xin Chen, Yuzhe Ji, Qingye Zhao, Zhengfeng Yang, Wang Lin, Enyi Tang, Qiguang Chen, and Xuandong Li. Synthesizing barrier certificates of neural network controlled continuous systems via approximations. In DAC , pages 631--636. IEEE , 2021. doi:10.1109/DAC18074.2021.9586327

    work page doi:10.1109/dac18074.2021.9586327 2021

  30. [30]

    Control barrier functions for mechanical systems: Theory and application to robotic grasping

    Wenceslao Shaw - Cortez, Denny Oetomo, Chris Manzie, and Peter Choong. Control barrier functions for mechanical systems: Theory and application to robotic grasping. IEEE Trans. Control. Syst. Technol. , 29 0 (2): 0 530--545, 2021. doi:10.1109/TCST.2019.2952317

    work page doi:10.1109/tcst.2019.2952317 2021

  31. [31]

    Neural network verification with branch-and-bound for general nonlinearities

    Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho - Jui Hsieh, and Huan Zhang. Neural network verification with branch-and-bound for general nonlinearities. In TACAS (1) , volume 15696 of Lecture Notes in Computer Science, pages 315--335. Springer, 2025. doi:10.1007/978-3-031-90643-5_17

    work page doi:10.1007/978-3-031-90643-5_17 2025

  32. [32]

    Series of abstractions for hybrid automata

    Ashish Tiwari and Gaurav Khanna. Series of abstractions for hybrid automata. In HSCC , volume 2289 of Lecture Notes in Computer Science, pages 465--478. Springer, 2002. doi:10.1007/3-540-45873-5_36

    work page doi:10.1007/3-540-45873-5_36 2002

  33. [33]

    Wabersich, Andrew J

    Kim P. Wabersich, Andrew J. Taylor, Jason J. Choi, Koushil Sreenath, Claire J. Tomlin, Aaron D. Ames, and Melanie N. Zeilinger. Data-driven safety filters: Hamilton-jacobi reachability, control barrier functions, and predictive methods for uncertain systems. IEEE Control Systems Magazine, 43 0 (5): 0 137--177, 2023. doi:10.1109/MCS.2023.3291885

    work page doi:10.1109/mcs.2023.3291885 2023

  34. [34]

    Assessing Safety for Control Systems Using Sum -of- Squares Programming

    Han Wang, Kostas Margellos, and Antonis Papachristodoulou. Assessing Safety for Control Systems Using Sum -of- Squares Programming . In Polynomial Optimization , Moments , and Applications , volume 206, pages 207--234. Springer Nature Switzerland, Cham, 2023. ISBN 978-3-031-38658-9 978-3-031-38659-6. doi:10.1007/978-3-031-38659-6_7

    work page doi:10.1007/978-3-031-38659-6_7 2023

  35. [35]

    Robust explanation constraints for neural networks

    Matthew Wicker, Juyeon Heo, Luca Costabello, and Adrian Weller. Robust explanation constraints for neural networks. In ICLR . OpenReview.net, 2023

    work page 2023

  36. [36]

    High-order control barrier functions

    Wei Xiao and Calin Belta. High-order control barrier functions. IEEE Trans. Autom. Control. , 67 0 (7): 0 3655--3662, 2022. doi:10.1109/TAC.2021.3105491

    work page doi:10.1109/tac.2021.3105491 2022

  37. [37]

    Darboux-type barrier certificates for safety verification of nonlinear hybrid systems

    Xia Zeng, Wang Lin, Zhengfeng Yang, Xin Chen, and Lilei Wang. Darboux-type barrier certificates for safety verification of nonlinear hybrid systems. In EMSOFT , pages 11:1--11:10. ACM , 2016. doi:10.1145/2968478.2968484

    work page doi:10.1145/2968478.2968484 2016

  38. [38]

    Exact verification of relu neural control barrier functions

    Hongchao Zhang, Junlin Wu, Yevgeniy Vorobeychik, and Andrew Clark. Exact verification of relu neural control barrier functions. In NeurIPS, 2023

    work page 2023

  39. [39]

    Efficient neural network robustness certification with general activation functions

    Huan Zhang, Tsui - Wei Weng, Pin - Yu Chen, Cho - Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In NeurIPS, pages 4944--4953, 2018

    work page 2018

  40. [40]

    Synthesizing barrier certificates using neural networks

    Hengjun Zhao, Xia Zeng, Taolue Chen, and Zhiming Liu. Synthesizing barrier certificates using neural networks. In HSCC , pages 25:1--25:11. ACM , 2020. doi:10.1145/3365365.3382222

    work page doi:10.1145/3365365.3382222 2020

  41. [41]

    Verifying neural network controlled systems using neural networks

    Qingye Zhao, Xin Chen, Zhuoyu Zhao, Yifan Zhang, Enyi Tang, and Xuandong Li. Verifying neural network controlled systems using neural networks. In HSCC , pages 3:1--3:11. ACM , 2022. doi:10.1145/3501710.3519511

    work page doi:10.1145/3501710.3519511 2022

  42. [42]

    Henzinger, and Krishnendu Chatterjee

    Dorde Zikelic, Mathias Lechner, Thomas A. Henzinger, and Krishnendu Chatterjee. Learning control policies for stochastic systems with reach-avoid guarantees. In AAAI , pages 11926--11935. AAAI Press, 2023. doi:10.1609/AAAI.V37I10.26407

    work page doi:10.1609/aaai.v37i10.26407 2023