---
OA_place: repository
OA_type: green
_id: '21091'
abstract:
- lang: eng
  text: 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.
acknowledgement: 'This work is supported by the European Research Council under Grant
  No.: ERC-2020-AdG 101020093.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Konstantin
  full_name: Kueffner, Konstantin
  id: 8121a2d0-dc85-11ea-9058-af578f3b4515
  last_name: Kueffner
  orcid: 0000-0001-8974-2542
- first_name: Zhengqi
  full_name: Yu, Zhengqi
  id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
  last_name: Yu
  orcid: 0000-0002-4993-773X
citation:
  ama: 'Henzinger TA, Kueffner K, Yu E. Formal verification of neural certificates
    done dynamically. In: <i>25th International Conference on Runtime Verification</i>.
    Vol 16087. Springer Nature; 2025:54-72. doi:<a href="https://doi.org/10.1007/978-3-032-05435-7_4">10.1007/978-3-032-05435-7_4</a>'
  apa: 'Henzinger, T. A., Kueffner, K., &#38; Yu, E. (2025). Formal verification of
    neural certificates done dynamically. In <i>25th International Conference on Runtime
    Verification</i> (Vol. 16087, pp. 54–72). Graz, Austria: Springer Nature. <a href="https://doi.org/10.1007/978-3-032-05435-7_4">https://doi.org/10.1007/978-3-032-05435-7_4</a>'
  chicago: Henzinger, Thomas A, Konstantin Kueffner, and Emily Yu. “Formal Verification
    of Neural Certificates Done Dynamically.” In <i>25th International Conference
    on Runtime Verification</i>, 16087:54–72. Springer Nature, 2025. <a href="https://doi.org/10.1007/978-3-032-05435-7_4">https://doi.org/10.1007/978-3-032-05435-7_4</a>.
  ieee: T. A. Henzinger, K. Kueffner, and E. Yu, “Formal verification of neural certificates
    done dynamically,” in <i>25th International Conference on Runtime Verification</i>,
    Graz, Austria, 2025, vol. 16087, pp. 54–72.
  ista: 'Henzinger TA, Kueffner K, Yu E. 2025. Formal verification of neural certificates
    done dynamically. 25th International Conference on Runtime Verification. RV: Runtime
    Verification, LNCS, vol. 16087, 54–72.'
  mla: Henzinger, Thomas A., et al. “Formal Verification of Neural Certificates Done
    Dynamically.” <i>25th International Conference on Runtime Verification</i>, vol.
    16087, Springer Nature, 2025, pp. 54–72, doi:<a href="https://doi.org/10.1007/978-3-032-05435-7_4">10.1007/978-3-032-05435-7_4</a>.
  short: T.A. Henzinger, K. Kueffner, E. Yu, in:, 25th International Conference on
    Runtime Verification, Springer Nature, 2025, pp. 54–72.
conference:
  end_date: 2025-09-19
  location: Graz, Austria
  name: 'RV: Runtime Verification'
  start_date: 2025-09-15
corr_author: '1'
date_created: 2026-01-29T16:03:01Z
date_published: 2025-09-13T00:00:00Z
date_updated: 2026-02-16T11:53:25Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-032-05435-7_4
ec_funded: 1
external_id:
  arxiv:
  - '2507.11987'
intvolume: '     16087'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.48550/arXiv.2507.11987
month: '09'
oa: 1
oa_version: Preprint
page: 54-72
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 25th International Conference on Runtime Verification
publication_identifier:
  eisbn:
  - '9783032054357'
  eissn:
  - 1611-3349
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Formal verification of neural certificates done dynamically
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16087
year: '2025'
...