Pith. sign in

REVIEW 4 major objections 4 minor 36 references

Formal Verification of Neural Certificates Done Dynamically

T0 review · 4 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper claims that a runtime monitor can certify safety of a neural-certificate-controlled system over a finite horizon without static verification of the entire state space or access to the controller, provided the local abstraction…

desk verdict A sensible modular idea for online certificate checking, but the soundness theorem rests on subroutine contracts that the concrete algorithms never prove, plus a missing base case; the formal claims do not hold as written. read the letter →

arxiv 2507.11987 v1 pith:R7WOPLBH submitted 2025-07-16 cs.SC cs.AI

Thomas A. Henzinger , Konstantin Kueffner , Emily Yu This is my paper · ORCID
classification cs.SCcs.AI
keywords runtimemonitoringneuralcertificatescontrolbarrierfunctionsReLUnetworksformalverificationreachabilityoverapproximationcyber-physicalsystemssatelliterendezvous
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper proposes shifting certificate verification from a one-time, exhaustive offline check over the whole state space to a lightweight runtime monitor that re-verifies the certificate locally at every observation step. The monitor observes the current trajectory, uses a local abstraction to over-approximate all states reachable within a finite lookahead horizon $h$, and runs a verifier on that region; if the verifier accepts, the certificate is guaranteed to hold on the actual trace up to that horizon. The central soundness theorem says that this guarantee is valid whenever the abstraction contains the true reachable states, the verifier is exact on the region, and the verifier call finishes within one observation interval $\varepsilon$. If correct, the approach provides a formal safety guarantee during deployment while avoiding the exponential cost of exhaustive state-space verification, and it can also detect that a learned certificate is invalid before the system leaves the safe set.

What carries the argument

The load-bearing construction is the soundness argument in Algorithm 1, which combines a local abstraction function $\mathcal{A}$ satisfying Eq. (3) — the true trace stays inside the predicted region for the horizon — with a verifier $\mathcal{V}$ satisfying Eq. (4), meaning a positive verdict is equivalent to the certificate condition holding on the region. The timing invariant is what makes the monitor sound: if the verifier call for horizon $2\varepsilon + h$ finishes in less than $\varepsilon$ time, then each positive verdict covers the next observation interval, so warnings arrive before the system can enter an uncertified region. For ReLU-based barrier functions, the verifier works on cubes, regions of constant neuron activation pattern under the rectified linear unit, and reduces the certificate conditions to linear inequalities on each cube.

What would settle it

Run the monitor on a system for which the exact certificate conditions are known on a single activation-pattern cube, and compare the verdict of VerifyCubesOnBoundary with an independent exact feasibility check of the Definition 2 inequalities over that cube; any false positive or false negative on a cube the monitor actually inspects refutes Eq. (4) and with it the soundness of the instantiated monitor.

Watch

Extended reading notes

Core claim

The paper's central claim is that formal verification of neural certificates can be done dynamically: instead of proving once and for all that the certificate satisfies its defining conditions on the entire state space, one proves those conditions on an over-approximation of the states the system will actually visit in the next $h$ time units, and repeats this step at every observation tick. Theorem 1 states that the resulting monitor is sound — a positive verdict at time $t$ implies the certificate condition holds on the trace up to time $t+h$ — provided the abstraction satisfies Eq. (3), the verifier satisfies Eq. (4), and the subroutine Next completes in less than the observation period $\varepsilon$. This turns certificate verification from a static, global task into a repeated, local one, and it is instantiated for ReLU-based control barrier functions through a verifier that searches activation-pattern cubes on the certificate boundary.

Load-bearing premise

The monitor's verdict is only as trustworthy as the concrete verifier: the paper assumes, by construction rather than by proof, that VerifyCubesOnBoundary returns 1 exactly when the ReLU-CBF conditions hold on the lookahead region; if the cube search, binary search, or neighborhood expansion is incomplete, a positive verdict carries no formal safety guarantee.

Editorial extensions

If this is right

  • A neural-certificate-controlled system can be kept safe during deployment even when static verification of the full state space is infeasible, as long as a sound local abstraction and an exact region verifier are available.
  • Certificate violations are detected ahead of time, so a fail-safe mechanism can be triggered while the system is still inside the certified region.
  • The same monitor works as a testing tool: an incorrect certificate is exposed quickly when the lookahead horizon is long enough, supplying counterexamples for a learner-monitor repair loop.
  • In the satellite rendezvous case study, per-step monitoring overhead stays below 16 ms against a 0.1 s control interval, while static verification of an 8-layer certificate timed out after two hours.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Because Theorem 1 treats the verifier as a black box, the same monitor could be instantiated with any exact set-based verifier, for example one built on mixed-integer linear programming, rather than the cube-search verifier demonstrated here.
  • The soundness theorem is stated for deterministic traces; a natural extension would replace the abstraction's containment guarantee with a probabilistic one, making the monitor's verdict correct with high confidence instead of certainty.
  • The cost of monitoring is tied to the volume of the lookahead cone rather than the volume of the state space, so the approach should scale to higher dimensions if the local abstraction stays tight, which could be tested by measuring verification time as state dimension grows.
  • The paper gives no proof that the concrete cube search satisfies Eq. (4); a direct extension would be to specify VerifyCubesOnBoundary formally and prove that the binary search, neighborhood expansion, and cube checks are sound and complete.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper proposes a runtime monitoring framework that, given a local abstraction function A satisfying Eq. (3) and a verifier V satisfying Eq. (4), guarantees (Theorem 1) that a positive monitor verdict implies certificate validity over a finite lookahead horizon h. The framework is instantiated for ReLU-based control barrier functions: Algorithm 3 builds a cone over-approximating reachable states, and Algorithm 4 verifies the certificate on activation cubes found near the barrier boundary. Experiments on a satellite rendezvous example report low per-step monitoring overhead and demonstrate that violations are detected for certificates that fail static verification.

Significance. The modular decomposition of runtime safety into an abstraction step and a verifier step is clean, and the idea of verifying certificates only along the executed trace is practically attractive. If the formal claims were fully discharged, the framework would be a useful complement to static verification for neural-certificate-controlled systems. The paper correctly acknowledges that the general theorem is conditional on Eqs. (3) and (4), and the experimental overheads are encouraging. However, for the concrete ReLU instantiation, neither Eq. (3) nor Eq. (4) is proved, and the proof of Theorem 1 has a base-case gap; the formal verification promise is therefore not yet established.

major comments (4)
  1. [Section 3.1, Theorem 1 and Algorithm 1] The proof of Theorem 1 begins the induction at k=0 with the sentence 'we assume we have already verified the first ε+h time interval,' but Algorithm 1's Init only sets v0 ← 1 and w0 ← x, and Algorithm 2's Init likewise performs no initial verification. As written, the monitor returns verdict 1 at time 0 before any condition on w[0,h) has been checked, so the base case of the induction is missing. The monitor must either perform an explicit initial verification of the first ε+h interval, with its cost included in the timing assumption, or the theorem statement and Algorithms 1 and 2 must be revised accordingly.
  2. [Section 4, Eq. (4) and Algorithm 4] The paper never proves that VerifyCubesOnBoundary satisfies Eq. (4). In particular, BinarySearch at line 2 is not shown to find a cube on the boundary B(x)=0; VerifyLinear is only described as 'Check conditions in Def. 2' and is never defined; the 1-bit Hamming BFS is not shown to visit every activation cube that intersects the lookahead cone; and the global 'Verified' set used at line 15 of Algorithm 4 is not initialized or updated. Since Lemma 1 and Theorem 1 both depend on V satisfying Eq. (4), the concrete monitor's formal soundness claim is unproven.
  3. [Section 4, Eq. (3) and Algorithm 3] ConstructCone uses an unspecified expand(cone) operation, and the paper provides no proof that the returned cone contains all reachable states up to horizon h. Without a rigorous definition of expand and a proof of the containment property, the instantiation does not establish Eq. (3), which is the other hypothesis of Theorem 1.
  4. [Section 2, Definition 2] Definition 2 is presented as a characterization of ReLU-based control barrier functions, but the paper does not prove that its conditions imply the standard CBF inequality ∇B(x)(f(x)+g(x)π(x)) ≥ 0 on C ∩ X(A), nor is the quantifier 'there exists an activation pattern A' reconciled with the need for a global safety argument on all of C. The verifier's correctness rests on this characterization, so the exact lemma used by VerifyLinear should be stated and proved or precisely referenced with a formal statement.
minor comments (4)
  1. [Table 2] In Table 2, the verified rows for the 8x16 and 16x16 configurations report numbers of traces that decrease with increasing horizon even though no violations are indicated, and for several horizons the verified and failed trace counts do not sum to the stated total of 323 (e.g., 292 + 26 = 318, not 323). These numbers should be reconciled and explained.
  2. [Section 5] The text says 'a verifier operating on the ReLU activation patterns as described in Section 5,' but the description of the verifier appears in Section 4.
  3. [Algorithm 4] The algorithm uses fail-safe() and Verified(c') without formal definitions; the fail-safe mechanism is never specified, and the persistent set of verified cubes is not included in the algorithm's state or initialization.
  4. [General presentation] There are minor language issues: 'If the the sub-routine Next can be computed' in Theorem 1, 'with epsilon ϵ' in Problem 1, and the notation M_h(w^epsilon_[0,t)) in Eq. (2) is typeset with malformed superscripts.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Theorem 1 is a conditional composition of explicitly stated subroutine assumptions; unproven verifier details are correctness gaps, not circular reductions.

full rationale

The paper's central claim (Theorem 1) is a conditional statement: if the abstraction A satisfies Eq. (3), the verifier V satisfies Eq. (4), and Next completes in less than epsilon time, then a positive monitor verdict implies phi(F,B,w[0,t+h))=1. These are hypotheses about the subroutines, not consequences of the monitor's definition, and they are not fitted to the target conclusion. Lemma 1 transfers the verifier's exactness (Eq. 4) to the actual trace using the abstraction containment (Eq. 3); this is a straightforward composition of assumed properties, not a derivation that reduces to its own input. The concrete ReLU instantiation leaves proof obligations open: no theorem is given that VerifyCubesOnBoundary or the unspecified expand(cone) satisfy Eqs. (3)-(4), and the proof of Theorem 1 states, 'We assume we have already verified the first epsilon+h time interval,' although Algorithm 1's Init performs no such verification. These are completeness and correctness gaps in the formal argument, but they are not circularity: the claims are not true by construction, and no fitted parameter is renamed as a prediction. Citations to the authors' own prior work [14] and [32] point to existing building blocks and do not carry the soundness argument. Overall, no load-bearing circular step was found.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The framework introduces no fitted constants and no new physical entities. The lookahead horizon and observation frequency are user-chosen operational parameters. The central guarantee rests on the soundness of the abstraction, the exactness of the verifier, and a worst-case timing assumption; the paper states the first two as assumptions but does not prove them for the concrete ReLU instantiation.

assumptions (5)
  • domain assumption Abstraction function A satisfies Eq. (3): the true trace over the next h time units is contained in A(w^epsilon_[0,t), h).
    Invoked in Lemma 1 and Theorem 1. The paper states this as a defining property but does not prove it for the concrete cone construction; the experiments mention fixed-step unrolling with input bounds, whose soundness is not demonstrated.
  • domain assumption Verifier V satisfies Eq. (4): V(Y)=1 iff phi(F,B,Y)=1 for every region Y.
    Required for Lemma 1 and Theorem 1. This exactness condition is stronger than typical sound-only verifiers, and the paper gives no proof that the cube-based verifier in Algorithms 2-4 satisfies it.
  • domain assumption The Next subroutine completes in less than epsilon time in the worst case.
    Necessary for Theorem 1. The paper reports average per-step times below 16 ms (Figures 3-4) but no worst-case bound.
  • ad hoc to paper Definition 2 correctly captures ReLU-based CBF validity and the conditions checked in VerifyLinear are sufficient for safety inside a cube.
    The definition is adapted from [34] without proof of equivalence to Definition 1; the online verifier's correctness depends on it.
  • standard math Binary search between the current state and an unsafe point finds a point with B(x)=0.
    Algorithm 4 relies on continuity of the ReLU network and a sign change along the segment; these are standard properties.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formal Verification of Neural Certificates Done Dynamically." pith.science (2026). https://pith.science/paper/R7WOPLBH

@misc{pith2026250711987,
  author       = {Pith},
  title        = {Pith review of: Formal Verification of Neural Certificates Done Dynamically},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/R7WOPLBH}},
  note         = {Machine review of arXiv:2507.11987}
}
read the original abstract

Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.

Figures

Figures reproduced from arXiv: 2507.11987 by the authors.

Figure 1
Figure 1. Overview of our monitoring framework. At runtime, the monitor observes sys￾tem states and computes an overapproximation of the reachable region using a local abstraction function. We do not assume access to the controller. A verifier checks whether the certificate remains valid in the lookahead region. If a violation is detected, a warning is issued and a fail-safe mechanism can be triggered [PITH_FULL_IMAGE:figure… view at source ↗
Figure 2
Figure 2. Illustration of online verification with lookahead. At each time step, the monitor maintains a cone that over-approximates the reachable states within a fixed horizon. If this cone intersects the unsafe region, the monitor searches for a cube on the barrier boundary where B(x) = 0. The cone is then shrunk to contain this boundary, and the identified cube along with its neighbors are verified to assess certificate va… view at source ↗
Figure 3
Figure 3. Monitoring overhead measured for lookahead horizons up to 200 steps, across four network configurations with varying depth and width. All configurations were successfully verified through static analysis (see [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Monitoring overhead measured for lookahead horizons up to 200 steps, across four network configurations with varying depth and width. Two CBFs failed static verification (one of them timed out), and our monitor successfully detected violations online in both cases, wit…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

36 extracted references · 33 canonical work pages

  1. [34]

    Advances in neural information processing systems36, 5685–5705 (2023)

    Zhang, H., Wu, J., Vorobeychik, Y., Clark, A.: Exact verification of relu neural control barrier functions. Advances in neural information processing systems36, 5685–5705 (2023)

    work page 2023

  2. [1]

    In: Proceedings of the 24th international conference on hybrid systems: computation and control

    Abate, A., Ahmed, D., Edwards, A., Giacobbe, M., Peruffo, A.: Fossil: a software tool for the formal synthesis of lyapunov functions and barrier certificates using neural networks. In: Proceedings of the 24th international conference on hybrid systems: computation and control. pp. 1–11 (2021)

    work page 2021

  3. [2]

    Heliyon 4(11) (2018)

    Abiodun, O.I., Jantan, A., Omolara, A.E., Dada, K.V., Mohamed, N.A., Arshad, H.: State-of-the-art in artificial neural network applications: A survey. Heliyon 4(11) (2018)

    work page 2018

  4. [3]

    In: 53rd IEEE conference on decision and control

    Ames, A.D., Grizzle, J.W., Tabuada, P.: Control barrier function based quadratic programs with application to adaptive cruise control. In: 53rd IEEE conference on decision and control. pp. 6271–6278. IEEE (2014)

    work page 2014

  5. [4]

    Journal of medical systems 42, 1–13 (2018)

    Anwar, S.M., Majid, M., Qayyum, A., Awais, M., Alnowami, M., Khan, M.K.: Medical image analysis using convolutional neural networks: a review. Journal of medical systems 42, 1–13 (2018)

    work page 2018

  6. [5]

    In: International conference on tools and algo- rithms for the construction and analysis of systems

    Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis: Runtime enforcement for reactive systems. In: International conference on tools and algo- rithms for the construction and analysis of systems. pp. 533–548. Springer (2015)

    2015

  7. [6]

    Advances in neural information processing systems32 (2019)

    Chang, Y.C., Roohi, N., Gao, S.: Neural lyapunov control. Advances in neural information processing systems32 (2019)

    work page 2019

  8. [7]

    In: TACAS (1)

    Chatterjee, K., Henzinger, T.A., Lechner, M., Zikelic, D.: A learner-verifier frame- work for neural network controllers and certificates of stochastic systems. In: TACAS (1). Lecture Notes in Computer Science, vol. 13993, pp. 3–25. Springer (2023) 18 T. Henzinger et al

    work page 2023

Show all 36 references
  1. [8]

    In: 28th IEEE International Real-Time Systems Symposium (RTSS 2007)

    Crenshaw, T.L., Gunter, E., Robinson, C.L., Sha, L., Kumar, P.: The simplex ref- erence model: Limiting fault-propagation due to unreliable components in cyber- physical system architectures. In: 28th IEEE International Real-Time Systems Symposium (RTSS 2007). pp. 400–412. IEEE (2007)

    2007

  2. [9]

    IEEE Trans

    Dawson, C., Gao, S., Fan, C.: Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control. IEEE Trans. Robotics 39(3), 1749–1767 (2023)

    2023

  3. [10]

    In: Conference on Robot Learning

    Dawson, C., Qin, Z., Gao, S., Fan, C.: Safe nonlinear control using robust neu- ral lyapunov-barrier functions. In: Conference on Robot Learning. pp. 1724–1735. PMLR (2022)

    2022

  4. [11]

    In: 2019 49th An- nual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)

    Desai, A., Ghosh, S., Seshia, S.A., Shankar, N., Tiwari, A.: Soter: a runtime assurance framework for programming safe robotics systems. In: 2019 49th An- nual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). pp. 138–150. IEEE (2019)

    2019

  5. [12]

    In: The Thirty-eighth Annual Conference on Neural Information Processing Systems (2024)

    Giacobbe, M., Kroening, D., Pal, A., Tautschnig, M.: Neural model checking. In: The Thirty-eighth Annual Conference on Neural Information Processing Systems (2024)

    2024

  6. [13]

    Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2024),https: //www.gurobi.com

    2024

  7. [14]

    In: L4DC

    Henzinger, T.A., Kresse, F., Mallik, K., Yu, E., Zikelic, D.: Predictive monitor- ing of black-box dynamical systems. In: L4DC. Proceedings of Machine Learning Research, PMLR (2025)

    2025

  8. [15]

    In: 2016 IEEE 55th Conference on Decision and Control (CDC)

    Jewison, C., Erwin, R.S.: A spacecraft benchmark problem for hybrid control and estimation. In: 2016 IEEE 55th Conference on Decision and Control (CDC). pp. 3300–3305. Ieee (2016)

    2016

  9. [16]

    IEEE transactions on neural networks and learning systems29(6), 2042–2062 (2017)

    Kiumarsi, B., Vamvoudakis, K.G., Modares, H., Lewis, F.L.: Optimal and au- tonomous control using reinforcement learning: A survey. IEEE transactions on neural networks and learning systems29(6), 2042–2062 (2017)

    2017

  10. [17]

    In: International Symposium on Model Checking Software

    Maderbacher, B., Schupp, S., Bartocci, E., Bloem, R., Ničković, D., Könighofer, B.: Provablecorrectandadaptivesimplexarchitectureforbounded-livenessproperties. In: International Symposium on Model Checking Software. pp. 141–160. Springer (2023)

    2023

  11. [18]

    In: # PLACE- HOLDER_PARENT_METADATA_VALUE#

    Mandal, U., Amir, G., Wu, H., Daukantas, I., Newell, F.L., Ravaioli, U.J., Meng, B., Durling, M., Ganai, M., Shim, T., et al.: Formally verifying deep rein- forcement learning controllers with lyapunov barrier certificates. In: # PLACE- HOLDER_PARENT_METADATA_VALUE#. pp. 95–10...

    2024

  12. [19]

    In: NASA formal methods symposium

    Mehmood, U., Sheikhi, S., Bak, S., Smolka, S.A., Stoller, S.D.: The black-box simplex architecture for runtime assurance of autonomous cps. In: NASA formal methods symposium. pp. 231–250. Springer (2022)

    2022

  13. [20]

    In: International conference on tools and algorithms for the construction and analysis of systems

    Peruffo, A., Ahmed, D., Abate, A.: Automated and formal synthesis of neural barrier certificates for dynamical models. In: International conference on tools and algorithms for the construction and analysis of systems. pp. 370–388. Springer (2021)

    2021

  14. [21]

    Formal Methods in System Design51, 62–86 (2017)

    Phan, D., Yang, J., Grosu, R., Smolka, S.A., Stoller, S.D.: Collision avoidance for mobilerobotswithlimitedsensingandlimitedinformationaboutmovingobstacles. Formal Methods in System Design51, 62–86 (2017)

    2017

  15. [22]

    IEEE Trans

    Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control.52(8), 1415–1428 (2007) Formal Verification of Neural Certificates Done Dynamically 19

    2007

  16. [23]

    Barron Associates, Inc

    Schierman, J.D., DeVore, M.D., Richards, N.D., Gandhi, N., Cooper, J.K., Horne- man, K.R., Stoller, S., Smolka, S.: Runtime assurance framework development for highly adaptive flight control systems. Barron Associates, Inc. Charlottesville, Tech. Rep (2015)

    2015

  17. [24]

    In: Proceedings of the 22nd IEEE/ACM international conference on Automated software engineering

    Sen, K.: Concolic testing. In: Proceedings of the 22nd IEEE/ACM international conference on Automated software engineering. pp. 571–572 (2007)

    2007

  18. [25]

    In: Haifa Verification Confer- ence

    Sen, K.: DART: directed automated random testing. In: Haifa Verification Confer- ence. Lecture Notes in Computer Science, vol. 6405, p. 4. Springer (2009)

    2009

  19. [26]

    In: ESEC/SIGSOFT FSE

    Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: ESEC/SIGSOFT FSE. pp. 263–272. ACM (2005)

    2005

  20. [27]

    ACC (IEEE Cat

    Seto, D., Krogh, B., Sha, L., Chutinan, A.: The simplex architecture for safe online controlsystemupgrades.In:Proceedingsofthe1998AmericanControlConference. ACC (IEEE Cat. No. 98CH36207). vol. 6, pp. 3504–3508. IEEE (1998)

    1998

  21. [28]

    Smith, M.C.: The general problem of the stability of motion : Translated and edited by a. t. fuller. taylor and francis, 1992. Autom.31(2), 353–354 (1995)

    1995

  22. [29]

    In: conference on Robot Learning

    Sun, D., Jha, S., Fan, C.: Learning certified control using contraction metric. In: conference on Robot Learning. pp. 1519–1539. PMLR (2021)

    2021

  23. [30]

    arXiv preprint arXiv:2403.19332 (2024)

    Tayal, M., Zhang, H., Jagtap, P., Clark, A., Kolathaya, S.: Learning a for- mally verified control barrier function in stochastic environment. arXiv preprint arXiv:2403.19332 (2024)

    2024 arXiv

  24. [31]

    IEEE Robotics and Automation Letters8(11), 7106–7113 (2023)

    Yin, J., Dawson, C., Fan, C., Tsiotras, P.: Shield model predictive path integral: A computationally efficient robust mpc method using control barrier functions. IEEE Robotics and Automation Letters8(11), 7106–7113 (2023)

    2023

  25. [32]

    In: Proceedings of the AAAI Conference on Artificial Intelligence

    Yu, E., Žikelić, Ð., Henzinger, T.A.: Neural control and certificate repair via run- time monitoring. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 39, pp. 26409–26417 (2025)

    2025

  26. [33]

    In: NeurIPS (2024)

    Zhang, H., Qin, Z., Gao, S., Clark, A.: SEEV: synthesis with efficient exact verifi- cation for relu neural barrier functions. In: NeurIPS (2024)

    2024

  27. [35]

    In: Proceedings of the 23rd international conference on hybrid systems: Computation and control

    Zhao, H., Zeng, X., Chen, T., Liu, Z.: Synthesizing barrier certificates using neural networks. In: Proceedings of the 23rd international conference on hybrid systems: Computation and control. pp. 1–11 (2020)

    2020

  28. [36]

    In: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control

    Zhao, Q., Chen, X., Zhao, Z., Zhang, Y., Tang, E., Li, X.: Verifying neural net- work controlled systems using neural networks. In: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control. pp. 1–11 (2022)

    2022

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.