---
res:
  bibo_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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-2985-7724
  - foaf_Person:
      foaf_givenName: Konstantin
      foaf_name: Kueffner, Konstantin
      foaf_surname: Kueffner
      foaf_workInfoHomepage: http://www.librecat.org/personId=8121a2d0-dc85-11ea-9058-af578f3b4515
    orcid: 0000-0001-8974-2542
  - foaf_Person:
      foaf_givenName: Zhengqi
      foaf_name: Yu, Zhengqi
      foaf_surname: Yu
      foaf_workInfoHomepage: http://www.librecat.org/personId=20aa2ae8-f2f1-11ed-bbfa-8205053f1342
    orcid: 0000-0002-4993-773X
  bibo_doi: 10.1007/978-3-032-05435-7_4
  bibo_volume: 16087
  dct_date: 2025^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/0302-9743
  - http://id.crossref.org/issn/1611-3349
  dct_language: eng
  dct_publisher: Springer Nature@
  dct_title: Formal verification of neural certificates done dynamically@
...
