pith. sign in

arxiv: 2605.20108 · v1 · pith:H5CQHMAInew · submitted 2026-05-19 · 📡 eess.SY · cs.AI· cs.LG· cs.LO· cs.SY

k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics

Ben Wooding , Hongchao Zhang , Taylor T. Johnson , Abolfazl Lavaei This is my paper

Pith reviewed 2026-05-20 03:35 UTC · model grok-4.3

classification 📡 eess.SY cs.AIcs.LGcs.LOcs.SY
keywords barrier certificatesneural networksdata-driven verificationnonlinear dynamicssafety certificationunknown systemsinductive synthesis
0
0 comments X

The pith

k-inductive neural barrier certificates certify safety for nonlinear systems with partially unknown dynamics from a single observed trajectory.

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

The paper shows how to build safety certificates for nonlinear systems whose equations are not fully known. Traditional certificates demand that a safety function never increases from one step to the next, but the k-inductive version tolerates a small rise for up to k-1 steps before it must decrease again. Neural networks represent these certificates because they handle large state spaces, yet they must still be checked for correctness through an iterative search that uses logical solvers. The method replaces the missing equations with a representation built directly from one recorded state sequence, allowing the logical check to run without loss of precision. This combination matters because many real control tasks lack exact models yet still need formal safety guarantees.

Core claim

k-inductive neural barrier certificates relax the strict non-increasing requirement of ordinary barrier certificates by permitting the function to rise by at most epsilon for up to k-1 consecutive steps while still guaranteeing that unsafe states are never reached. For systems whose dynamics are only partially known, a data-driven representation constructed from one state trajectory supplies the necessary model information to an SMT solver inside a counterexample-guided synthesis loop. This representation supports verification without restricting the certificate to sum-of-squares or other fixed function families, and the overall procedure is demonstrated on three nonlinear examples.

What carries the argument

The k-inductive neural barrier certificate, which encodes a relaxed safety condition allowing bounded temporary increases over k steps, together with a data-driven representation of the unknown dynamics derived from a single trajectory that is used directly inside the SMT-based verification loop.

If this is right

  • Safety verification becomes feasible for systems where only trajectory measurements are available rather than analytic equations.
  • The k-inductive relaxation reduces the conservatism that arises when a barrier function is forced to decrease at every single step.
  • Neural networks can serve as barrier functions without being limited to polynomial or sum-of-squares forms.
  • The counterexample-guided loop can continue using only the trajectory-derived model without requiring additional model identification steps.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same single-trajectory representation could support online updates when new measurements arrive during operation.
  • Similar data-driven modeling may extend the approach to verifying other properties such as reachability or stability.
  • The method suggests that trajectory data collected from physical experiments can substitute for first-principles models in formal safety arguments.

Load-bearing premise

One recorded state trajectory yields a data-driven model that is accurate enough for the SMT solver to produce sound safety verdicts inside the synthesis loop.

What would settle it

A concrete state sequence that is consistent with the recorded trajectory data yet reaches an unsafe region or violates the k-inductive barrier condition would demonstrate that the certificate does not guarantee safety.

Figures

Figures reproduced from arXiv: 2605.20108 by Abolfazl Lavaei, Ben Wooding, Hongchao Zhang, Taylor T. Johnson.

Figure 1
Figure 1. Figure 1: Safety illustration: The black trajec￾tory, starting in the initial region XI ⊂ X, may temporarily increase (crossing the blue-dashed 0- level set) as long as it decreases within k steps and never exceeds the red level set λ = (k − 1)ϵ. This ensures it does not reach the unsafe region XU ⊂ X, where XI ∩ XU = ∅. candidate using SMT solvers is computationally more efficient than directly searching for a solu… view at source ↗
Figure 2
Figure 2. Figure 2: The CEGIS procedure for verification with k-NBCs. Data points s ∈ S are sampled from the state space X. The Learner then gen￾erates a candidate k-NBC B(·) based on the dataset triple (S, S+, Sk+). The Verifier checks if the candidate k-NBC is valid for all states x ∈ X. If B(·) is invalid, any counterexam￾ples c ∈ C are added to the dataset and the Learner generates a new can￾didate. The process is repeate… view at source ↗
Figure 3
Figure 3. Figure 3: k-NBC results for the highly nonlinear system. (a) Candidate k-NBC showing violations where XI and XU intersect the level sets. Sampled points are depicted in brown. (b) Verified k￾NBC after retraining with counterexamples (black points). Both show the zero level set in dashed blue, unsafe level set in red, and true vector field in gray. If the above logical formula is satisfied, the SMT solver returns sat… view at source ↗
Figure 4
Figure 4. Figure 4: Verified k-NBC for the polynomial system, with the zero level set shown in dashed blue and the unsafe level set in red. Origi￾nal sampled points are depicted in brown, while counterexamples are in black. The k-NBC was identified in the 7th iteration. The contour plot represents barrier certificate values across all states, and the true vector field is illustrated in gray. Appendix C. Additional Case Studie… view at source ↗
Figure 5
Figure 5. Figure 5: Verified k-NBC for the pendulum system, with the zero level set in dashed blue and the unsafe level set in red. Original sampled points are shown in brown, and counterexamples in black. The k-NBC was obtained af￾ter one retraining. The con￾tour plot illustrates barrier cer￾tificate values across all states, while the true vector field is depicted in gray. System Description. For our second case study, we c… view at source ↗
read the original abstract

While conventional (k=1) discrete-time barrier certificate conditions impose strict safety constraints by requiring the function to be non-increasing at every step, k-inductive barrier certificates relax this by allowing a temporary increase -- up to k-1 times, each within a threshold $\epsilon$ -- while maintaining overall safety, and improving flexibility. This paper leverages neural networks and constructs k-inductive neural barrier certificates (k-NBCs) for (partially) unknown nonlinear systems. While neural networks offer scalability in the design process, they lack formal guarantees, requiring additional approaches such as counterexample-guided inductive synthesis (CEGIS) with satisfiability modulo theories (SMT) for verification. However, the CEGIS-SMT framework requires knowledge of system dynamics, which is unavailable in practical settings. To address this, we leverage the generalization of the Willems et al.'s fundamental lemma, using a single state trajectory, to construct a data-driven representation of (partially) unknown models for SMT verification without sacrificing accuracy. Additionally, CEGIS-SMT further removes the constraint of restricting barrier certificates to specific function classes, such as sum-of-squares, enabling greater flexibility in their design. We validate our approach on three nonlinear case studies with (partially) unknown dynamics.

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

2 major / 2 minor

Summary. The paper proposes synthesizing k-inductive neural barrier certificates (k-NBCs) for partially unknown nonlinear discrete-time systems. It generalizes Willems et al.'s fundamental lemma to obtain a data-driven behavioral representation of the dynamics from a single observed state trajectory, then substitutes this representation for the unknown model inside a CEGIS-SMT loop to verify the relaxed k-inductive barrier conditions (temporary increases bounded by epsilon allowed up to k-1 steps). The approach is illustrated on three nonlinear case studies.

Significance. If the single-trajectory data-driven representation can be shown to yield a sound (conservative or exact) encoding for SMT verification, the work would enable formal safety certificates for black-box or partially known nonlinear plants while retaining the design flexibility of neural networks and the relaxed k-inductive conditions. This would extend data-driven verification beyond linear systems and sum-of-squares barriers.

major comments (2)
  1. [Abstract and §3] Abstract and §3 (data-driven representation): the claim that the generalized fundamental lemma produces a representation 'without sacrificing accuracy' for SMT verification is load-bearing for the soundness of the entire CEGIS loop, yet the manuscript supplies no error bounds, persistency-of-excitation conditions for the nonlinear terms, or independent checks that the single trajectory spans the relevant state-input space. If any admissible continuation lies outside the data span, the SMT solver sees a strictly smaller set of next states than the true plant, allowing an unsafe k-NBC to be declared valid.
  2. [§4] §4 (CEGIS-SMT encoding): the substitution of the finite data-derived constraints into the k-inductive conditions (Eq. for the barrier decrease with up to k-1 epsilon-bounded increases) requires an explicit argument that the encoding is conservative with respect to the unknown nonlinear dynamics; without it, the verification result cannot be transferred to the real system.
minor comments (2)
  1. [§5] §5 (case studies): quantitative verification results, CEGIS iteration counts, solver times, and any observed counterexample statistics or violation rates should be reported to allow assessment of empirical support.
  2. [Notation] Notation throughout: the precise statement of the nonlinear generalization of the fundamental lemma (including any rank or excitation assumptions) should be stated as a numbered lemma or proposition with a reference to the original Willems result.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback, which helps clarify important aspects of soundness in our data-driven approach. We address the two major comments point by point below and will revise the manuscript to incorporate the requested clarifications and arguments.

read point-by-point responses

  1. Referee: [Abstract and §3] Abstract and §3 (data-driven representation): the claim that the generalized fundamental lemma produces a representation 'without sacrificing accuracy' for SMT verification is load-bearing for the soundness of the entire CEGIS loop, yet the manuscript supplies no error bounds, persistency-of-excitation conditions for the nonlinear terms, or independent checks that the single trajectory spans the relevant state-input space. If any admissible continuation lies outside the data span, the SMT solver sees a strictly smaller set of next states than the true plant, allowing an unsafe k-NBC to be declared valid.

    Authors: We acknowledge that the current manuscript does not explicitly state persistency-of-excitation conditions or provide error bounds for the nonlinear generalization of the fundamental lemma. The phrase 'without sacrificing accuracy' in the abstract refers to the fact that the data-driven representation exactly encodes the observed transitions from the single trajectory without introducing additional approximation errors beyond those inherent in the data collection itself. However, completeness of this representation with respect to all admissible behaviors of the unknown nonlinear dynamics does depend on the trajectory being sufficiently rich. In the revised version we will add a dedicated paragraph in §3 that (i) recalls the relevant persistency-of-excitation assumptions from the nonlinear behavioral-systems literature, (ii) states the precise condition under which the single-trajectory representation spans the full behavior, and (iii) notes that, when this condition holds, the SMT encoding sees exactly the same set of next states as the true plant. We will also add a short practical guideline on how to assess spanning (e.g., via hold-out trajectory segments) so that the soundness claim can be transferred to the real system. revision: yes

  2. Referee: [§4] §4 (CEGIS-SMT encoding): the substitution of the finite data-derived constraints into the k-inductive conditions (Eq. for the barrier decrease with up to k-1 epsilon-bounded increases) requires an explicit argument that the encoding is conservative with respect to the unknown nonlinear dynamics; without it, the verification result cannot be transferred to the real system.

    Authors: We agree that an explicit conservativeness argument is necessary. In the revised §4 we will insert a short proposition immediately after the encoding description. The proposition will state that, under the persistency-of-excitation condition added in §3, every next-state pair admitted by the data-derived constraints is admissible for the true plant, and conversely. Consequently, satisfaction of the k-inductive barrier inequalities over the data constraints implies satisfaction over the true dynamics. The proof sketch will rely on the exact behavioral equivalence guaranteed by the generalized fundamental lemma. If the collected trajectory fails the excitation condition, we will note that the resulting certificate remains valid only for the observed behaviors and recommend additional data collection; this caveat will be added to the discussion of the case studies as well. revision: yes

Circularity Check

0 steps flagged

No significant circularity: derivation relies on external lemma and raw data without self-referential reduction

full rationale

The paper's central construction applies the generalized Willems fundamental lemma (an external result) to a single observed trajectory to obtain a data-driven behavioral representation, which is then fed into an independent CEGIS-SMT loop for k-NBC verification. No step equates a fitted parameter or derived quantity back to itself by construction, nor does any load-bearing claim rest solely on a self-citation chain whose content is unverified outside the present work. The data trajectory serves as an independent input, and the lemma supplies the mapping to constraints without the paper re-deriving or renaming its own outputs as predictions. This satisfies the criteria for a self-contained derivation against external benchmarks.

Axiom & Free-Parameter Ledger

2 free parameters · 1 axioms · 0 invented entities

The method depends on the validity of the generalized fundamental lemma for the observed trajectory and on user-chosen parameters k and epsilon that control the allowed temporary violations.

free parameters (2)
  • k
    Induction depth; chosen by the designer to trade off flexibility against verification complexity.
  • epsilon
    Threshold on the allowed temporary increase of the barrier function.
axioms (1)
  • domain assumption Generalization of Willems fundamental lemma applies to the partially unknown nonlinear system from a single trajectory
    Invoked to obtain a data-driven model usable inside SMT verification without full dynamics knowledge.

pith-pipeline@v0.9.0 · 5774 in / 1224 out tokens · 36664 ms · 2026-05-20T03:35:57.352918+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

71 extracted references · 71 canonical work pages · 1 internal anchor

  1. [1]

    IEEE Transactions on Automatic Control , volume=

    Formal verification of unknown discrete-and continuous-time systems: A data-driven approach , author=. IEEE Transactions on Automatic Control , volume=. 2023 , publisher=

    work page 2023

  2. [2]

    arXiv preprint arXiv:2502.05510 , year=

    Data-Driven Neural Certificate Synthesis , author=. arXiv preprint arXiv:2502.05510 , year=

    work page arXiv

  3. [3]

    arXiv:2507.18131v2 , year=

    Data-driven model order reduction for continuous-and discrete-time nonlinear systems , author=. arXiv:2507.18131v2 , year=

    work page arXiv

  4. [4]

    Samari, A

    Data-driven control of large-scale networks with formal guarantees: A small-gain free approach , author=. arXiv: 2411.06743 , year=

    work page arXiv

  5. [5]

    Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , pages=

    Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models , author=. Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , pages=

    work page

  6. [6]

    International workshop on hybrid systems: Computation and control , pages=

    Safety verification of hybrid systems using barrier certificates , author=. International workshop on hybrid systems: Computation and control , pages=. 2004 , organization=

    work page 2004

  7. [7]

    arXiv preprint arXiv:2412.07232 , year=

    Learning k-Inductive Control Barrier Certificates for Unknown Nonlinear Dynamics Beyond Polynomials , author=. arXiv preprint arXiv:2412.07232 , year=

    work page arXiv

  8. [8]

    Anand, Mahathi and Murali, Vishnu and Trivedi, Ashutosh and Zamani, Majid , booktitle=

    work page

  9. [9]

    IFAC-PapersOnLine , volume=

    Formally verified neural network control barrier certificates for unknown systems , author=. IFAC-PapersOnLine , volume=. 2023 , publisher=

    work page 2023

  10. [10]

    CP–NCBF: A Conformal Prediction-based Approach to Synthesize Verified Neural Control Barrier Functions,

    Cp-ncbf: A conformal prediction-based approach to synthesize verified neural control barrier functions , author=. arXiv preprint arXiv:2503.17395 , year=

    work page arXiv

  11. [11]

    IEEE Transactions on Automatic Control , volume=

    Learning controllers from data via approximate nonlinearity cancellation , author=. IEEE Transactions on Automatic Control , volume=. 2023 , publisher=

    work page 2023

  12. [12]

    Learning for Dynamics and Control Conference , pages=

    Data-driven controller synthesis of unknown nonlinear polynomial systems via control barrier certificates , author=. Learning for Dynamics and Control Conference , pages=. 2022 , organization=

    work page 2022

  13. [13]

    SIAM Journal on Control and Optimization , volume=

    Convex programs for temporal verification of nonlinear dynamical systems , author=. SIAM Journal on Control and Optimization , volume=. 2007 , publisher=

    work page 2007

  14. [14]

    IFAC-PapersOnLine , volume=

    Data-based guarantees of set invariance properties , author=. IFAC-PapersOnLine , volume=. 2020 , publisher=

    work page 2020

  15. [15]

    Systems & Control Letters , volume=

    A note on persistency of excitation , author=. Systems & Control Letters , volume=. 2005 , publisher=

    work page 2005

  16. [16]

    Safety Verification of Dynamical Systems via k-Inductive Barrier Certificates , year=

    Anand, Mahathi and Murali, Vishnu and Trivedi, Ashutosh and Zamani, Majid , booktitle=. Safety Verification of Dynamical Systems via k-Inductive Barrier Certificates , year=

    work page

  17. [17]

    Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control , pages=

    K-inductive barrier certificates for stochastic systems , author=. Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control , pages=

    work page

  18. [18]

    2025 , organization=

    Wooding, Ben and Horbanov, Viacheslav and Lavaei, Abolfazl , booktitle=. 2025 , organization=

    work page 2025

  19. [19]

    Abate, Alessandro and Ahmed, Daniele and Edwards, Alec and Giacobbe, Mirco and Peruffo, Andrea , booktitle=

    work page

  20. [20]

    arXiv preprint arXiv:2304.02297 , year=

    Direct data-driven signal temporal logic control of linear systems , author=. arXiv preprint arXiv:2304.02297 , year=

    work page arXiv

  21. [21]

    Nonlinear Analysis: Hybrid Systems , volume=

    Data-driven abstraction-based control synthesis , author=. Nonlinear Analysis: Hybrid Systems , volume=. 2024 , publisher=

    work page 2024

  22. [22]

    2004 43rd IEEE conference on decision and control (CDC) , volume=

    Stochastic safety verification using barrier certificates , author=. 2004 43rd IEEE conference on decision and control (CDC) , volume=. 2004 , organization=

    work page 2004

  23. [23]

    IEEE Transactions on Automatic Control , volume=

    A framework for worst-case and stochastic safety verification using barrier certificates , author=. IEEE Transactions on Automatic Control , volume=. 2007 , publisher=

    work page 2007

  24. [24]

    IEEE Control Systems Letters , volume=

    A scenario approach for synthesizing k-inductive barrier certificates , author=. IEEE Control Systems Letters , volume=. 2022 , publisher=

    work page 2022

  25. [25]

    IFAC-PapersOnLine , volume=

    t-Barrier certificates: a continuous analogy to k-induction , author=. IFAC-PapersOnLine , volume=. 2018 , publisher=

    work page 2018

  26. [26]

    2019 , organization=

    Ames, Aaron D and Coogan, Samuel and Egerstedt, Magnus and Notomista, Gennaro and Sreenath, Koushil and Tabuada, Paulo , booktitle=. 2019 , organization=

    work page 2019

  27. [27]

    , journal=

    Lindemann, Lars and Dimarogonas, Dimos V. , journal=. Control Barrier Functions for Signal Temporal Logic Tasks , year=

    work page

  28. [28]

    IEEE Control Systems Letters , volume=

    Safety certification for stochastic systems via neural barrier functions , author=. IEEE Control Systems Letters , volume=. 2022 , publisher=

    work page 2022

  29. [29]

    Automatica , volume=

    Data-driven verification and synthesis of stochastic systems via barrier certificates , author=. Automatica , volume=. 2024 , publisher=

    work page 2024

  30. [30]

    IEEE Transactions on Automatic Control , volume=

    Formulas for data-driven control: Stabilization, optimality, and robustness , author=. IEEE Transactions on Automatic Control , volume=. 2019 , publisher=

    work page 2019

  31. [31]

    IEEE Control Systems Letters , volume=

    Willems’ fundamental lemma for state-space systems and its extension to multiple datasets , author=. IEEE Control Systems Letters , volume=. 2020 , publisher=

    work page 2020

  32. [32]

    IFAC-PapersOnLine , volume=

    Data-driven optimal output feedback control of linear systems from input-output data , author=. IFAC-PapersOnLine , volume=. 2023 , publisher=

    work page 2023

  33. [33]

    IEEE Transactions on Automatic Control , volume=

    Data-driven stabilization of nonlinear polynomial systems with noisy data , author=. IEEE Transactions on Automatic Control , volume=. 2021 , publisher=

    work page 2021

  34. [34]

    2015 54th IEEE conference on decision and control (CDC) , pages=

    A sublinear algorithm for barrier-certificate-based data-driven model validation of dynamical systems , author=. 2015 54th IEEE conference on decision and control (CDC) , pages=. 2015 , organization=

    work page 2015

  35. [35]

    IEEE Control Systems Letters , year=

    Data-driven synthesis of safety controllers via multiple control barrier certificates , author=. IEEE Control Systems Letters , year=

    work page

  36. [36]

    IEEE Transactions on Automatic Control , year=

    Data-driven models of monotone systems , author=. IEEE Transactions on Automatic Control , year=

    work page

  37. [37]

    International Conference on Computer Aided Verification , pages=

    DryVR: Data-driven verification and compositional reasoning for automotive systems , author=. International Conference on Computer Aided Verification , pages=. 2017 , organization=

    work page 2017

  38. [38]

    2022 IEEE 61st Conference on Decision and Control (CDC) , pages=

    Probabilistic guarantees on the objective value for the scenario approach via sensitivity analysis , author=. 2022 IEEE 61st Conference on Decision and Control (CDC) , pages=. 2022 , organization=

    work page 2022

  39. [39]

    2022 IEEE 61st Conference on Decision and Control (CDC) , pages=

    Adaptive sampling-based motion planning with control barrier functions , author=. 2022 IEEE 61st Conference on Decision and Control (CDC) , pages=. 2022 , organization=

    work page 2022

  40. [40]

    Automatica , volume=

    Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications , author=. Automatica , volume=. 2022 , publisher=

    work page 2022

  41. [41]

    Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control , pages=

    Formal safety verification of unknown continuous-time systems: a data-driven approach , author=. Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control , pages=

    work page

  42. [42]

    Proceedings of the AAAI Conference on Artificial Intelligence , volume=

    Sampling-based robust control of autonomous systems with non-gaussian noise , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

    work page

  43. [43]

    Journal of Artificial Intelligence Research , volume=

    Robust control for dynamical systems with non-gaussian noise via formal abstractions , author=. Journal of Artificial Intelligence Research , volume=

    work page

  44. [44]

    Hsieh, Chiao and Waga, Masaki and Suenaga, Kohei , booktitle=

    work page

  45. [45]

    Adam: A Method for Stochastic Optimization

    Adam: A method for stochastic optimization , author=. arXiv preprint arXiv:1412.6980 , year=

    work page internal anchor Pith review Pith/arXiv arXiv

  46. [46]

    IEEE Robotics and Automation Letters , volume=

    Model-free safe reinforcement learning through neural barrier certificate , author=. IEEE Robotics and Automation Letters , volume=. 2023 , publisher=

    work page 2023

  47. [47]

    Proceedings of the 23rd international conference on hybrid systems: Computation and control , pages=

    Synthesizing barrier certificates using neural networks , author=. Proceedings of the 23rd international conference on hybrid systems: Computation and control , pages=

    work page

  48. [48]

    Zhou, Ruikun and Quartz, Thanin and De Sterck, Hans and Liu, Jun , journal=

    work page

  49. [49]

    International conference on tools and algorithms for the construction and analysis of systems , pages=

    Automated and formal synthesis of neural barrier certificates for dynamical models , author=. International conference on tools and algorithms for the construction and analysis of systems , pages=. 2021 , organization=

    work page 2021

  50. [50]

    2013 , organization=

    Gao, Sicun and Kong, Soonho and Clarke, Edmund M , booktitle=. 2013 , organization=

    work page 2013

  51. [51]

    Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31 , pages=

    The marabou framework for verification and analysis of deep neural networks , author=. Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31 , pages=. 2019 , organization=

    work page 2019

  52. [52]

    Z3: An efficient

    De Moura, Leonardo and Bj. Z3: An efficient. International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=. 2008 , organization=

    work page 2008

  53. [53]

    2002 , organization=

    Prajna, Stephen and Papachristodoulou, Antonis and Parrilo, Pablo A , booktitle=. 2002 , organization=

    work page 2002

  54. [54]

    IEEE Transactions on automatic control , volume=

    The scenario approach to robust control design , author=. IEEE Transactions on automatic control , volume=. 2006 , publisher=

    work page 2006

  55. [55]

    2021 60th IEEE conference on decision and control (CDC) , pages=

    Fundamental lemma for data-driven analysis of linear parameter-varying systems , author=. 2021 60th IEEE conference on decision and control (CDC) , pages=. 2021 , organization=

    work page 2021

  56. [56]

    2018 , publisher=

    Introduction to the scenario approach , author=. 2018 , publisher=

    work page 2018

  57. [57]

    International Conference on Learning Representations , year=

    Learning safe multi-agent control with decentralized neural barrier certificates , author=. International Conference on Learning Representations , year=

    work page

  58. [58]

    IEEE Control Systems Letters , year=

    From a single trajectory to safety controller synthesis of discrete-time nonlinear polynomial systems , author=. IEEE Control Systems Letters , year=

    work page

  59. [59]

    Gardner, Jamie and Wooding, Ben and Nejati, Amy and Lavaei, Abolfazl , booktitle=

    work page

  60. [60]

    Proceedings of the AAAI Conference on Artificial Intelligence , volume=

    Neural closure certificates , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

    work page

  61. [61]

    2025 , organization=

    Debauche, Virginie and Edwards, Alec and Jungers, Raphael M and Abate, Alessandro , booktitle=. 2025 , organization=

    work page 2025

  62. [62]

    2023 , publisher=

    Garcez, Artur d’Avila and Lamb, Luis C , journal=. 2023 , publisher=

    work page 2023

  63. [63]

    2020 , publisher=

    Sum of Squares: Theory and Applications , author=. 2020 , publisher=

    work page 2020

  64. [64]

    2020 , publisher=

    Abate, Alessandro and Ahmed, Daniele and Giacobbe, Mirco and Peruffo, Andrea , journal=. 2020 , publisher=

    work page 2020

  65. [65]

    2023 , publisher=

    Dawson, Charles and Gao, Sicun and Fan, Chuchu , journal=. 2023 , publisher=

    work page 2023

  66. [66]

    SIAM review , volume=

    Atomic decomposition by basis pursuit , author=. SIAM review , volume=. 2001 , publisher=

    work page 2001

  67. [67]

    IEEE Transactions on information theory , volume=

    Compressed sensing , author=. IEEE Transactions on information theory , volume=. 2006 , publisher=

    work page 2006

  68. [68]

    Chaos: An Interdisciplinary Journal of Nonlinear Science , volume=

    Extended dynamic mode decomposition with dictionary learning: A data-driven adaptive spectral decomposition of the Koopman operator , author=. Chaos: An Interdisciplinary Journal of Nonlinear Science , volume=. 2017 , publisher=

    work page 2017

  69. [69]

    International conference on computational learning theory , pages=

    A generalized representer theorem , author=. International conference on computational learning theory , pages=. 2001 , organization=

    work page 2001

  70. [70]

    IEEE Control Systems Letters , volume=

    Robust adaptive control barrier functions: An adaptive and data-driven approach to safety , author=. IEEE Control Systems Letters , volume=. 2020 , publisher=

    work page 2020

  71. [71]

    doi:10.52202/079017-3214 , editor =

    Zhang, Hongchao and Qin, Zhizhen and Gao, Sicun and Clark, Andrew , booktitle =. doi:10.52202/079017-3214 , editor =

    work page doi:10.52202/079017-3214