---
OA_place: publisher
OA_type: hybrid
_id: '22006'
abstract:
- lang: eng
text: Runtime monitoring checks, during execution, whether a partial signal produced
by a hybrid system satisfies its specification. Signal First-Order Logic (SFO)
offers expressive real-time specifications over such signals, but currently comes
only with Boolean semantics and has no tool support. We provide the first robustness-based
quantitative semantics for SFO, enabling the expression and evaluation of rich
real-time properties beyond the scope of existing formalisms such as Signal Temporal
Logic. To enable online monitoring, we identify a past-time fragment of SFO and
give a pastification procedure that transforms bounded-response SFO formulas into
equisatisfiable formulas in this fragment. We then develop an efficient runtime
monitoring algorithm for this past-time fragment and evaluate its performance
on a set of benchmarks, demonstrating the practicality and effectiveness of our
approach. To the best of our knowledge, this is the first publicly available prototype
for online quantitative monitoring of full SFO.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported by the European Research Council (ERC) Grants VAMOS (No. 101020093)
and HYPER (No. 101055412), and by the Advanced Research and Invention Agency under
the Safeguarded AI programme (MSAI-PR01-P047).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- 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: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
citation:
ama: 'Chalupa M, Henzinger TA, Sarac NE, Yu E. Quantitative monitoring of Signal
First-Order logic. In: 27th International Symposium on Formal Methods.
Vol 16557. Springer Nature; 2026:214-233. doi:10.1007/978-3-032-26220-2_11'
apa: 'Chalupa, M., Henzinger, T. A., Sarac, N. E., & Yu, E. (2026). Quantitative
monitoring of Signal First-Order logic. In 27th International Symposium on
Formal Methods (Vol. 16557, pp. 214–233). Tokyo, Japan: Springer Nature. https://doi.org/10.1007/978-3-032-26220-2_11'
chicago: Chalupa, Marek, Thomas A Henzinger, Naci E Sarac, and Emily Yu. “Quantitative
Monitoring of Signal First-Order Logic.” In 27th International Symposium on
Formal Methods, 16557:214–33. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-26220-2_11.
ieee: M. Chalupa, T. A. Henzinger, N. E. Sarac, and E. Yu, “Quantitative monitoring
of Signal First-Order logic,” in 27th International Symposium on Formal Methods,
Tokyo, Japan, 2026, vol. 16557, pp. 214–233.
ista: 'Chalupa M, Henzinger TA, Sarac NE, Yu E. 2026. Quantitative monitoring of Signal
First-Order logic. 27th International Symposium on Formal Methods. FM: Formal
Methods, LNCS, vol. 16557, 214–233.'
mla: Chalupa, Marek, et al. “Quantitative Monitoring of Signal First-Order Logic.”
27th International Symposium on Formal Methods, vol. 16557, Springer Nature,
2026, pp. 214–33, doi:10.1007/978-3-032-26220-2_11.
short: M. Chalupa, T.A. Henzinger, N.E. Sarac, E. Yu, in:, 27th International Symposium
on Formal Methods, Springer Nature, 2026, pp. 214–233.
conference:
end_date: 2026-05-22
location: Tokyo, Japan
name: 'FM: Formal Methods'
start_date: 2026-05-18
das_tickbox: '0'
date_created: 2026-06-14T22:01:44Z
date_published: 2026-05-18T00:00:00Z
date_updated: 2026-06-22T08:21:09Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-032-26220-2_11
ec_funded: 1
external_id:
arxiv:
- '2603.00728'
file:
- access_level: open_access
checksum: 7055199ecb985e9e2e272f4988827067
content_type: application/pdf
creator: dernst
date_created: 2026-06-22T08:18:41Z
date_updated: 2026-06-22T08:18:41Z
file_id: '22113'
file_name: 2026_LNCS_Chalupa.pdf
file_size: 849237
relation: main_file
success: 1
file_date_updated: 2026-06-22T08:18:41Z
has_accepted_license: '1'
intvolume: ' 16557'
keyword:
- Signal first-order logic
- Robustness-based quantitative semantics
- Online runtime monitoring
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '05'
oa: 1
oa_version: Published Version
page: 214-233
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 27th International Symposium on Formal Methods
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032262196'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative monitoring of Signal First-Order logic
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16557
year: '2026'
...
---
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: 25th International Conference on Runtime Verification.
Vol 16087. Springer Nature; 2025:54-72. doi:10.1007/978-3-032-05435-7_4'
apa: 'Henzinger, T. A., Kueffner, K., & Yu, E. (2025). Formal verification of
neural certificates done dynamically. In 25th International Conference on Runtime
Verification (Vol. 16087, pp. 54–72). Graz, Austria: Springer Nature. https://doi.org/10.1007/978-3-032-05435-7_4'
chicago: Henzinger, Thomas A, Konstantin Kueffner, and Emily Yu. “Formal Verification
of Neural Certificates Done Dynamically.” In 25th International Conference
on Runtime Verification, 16087:54–72. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05435-7_4.
ieee: T. A. Henzinger, K. Kueffner, and E. Yu, “Formal verification of neural certificates
done dynamically,” in 25th International Conference on Runtime Verification,
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.” 25th International Conference on Runtime Verification, vol.
16087, Springer Nature, 2025, pp. 54–72, doi:10.1007/978-3-032-05435-7_4.
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'
...
---
OA_place: repository
OA_type: green
_id: '19668'
abstract:
- lang: eng
text: Learning-based methods provide a promising approach to solving highly non-linear
control tasks that are often challenging for classical control methods. To ensure
the satisfaction of a safety property, learning-based methods jointly learn a
control policy together with a certificate function for the property. Popular
examples include barrier functions for safety and Lyapunov functions for asymptotic
stability. While there has been significant progress on learning-based control
with certificate functions in the white-box setting, where the correctness of
the certificate function can be formally verified, there has been little work
on ensuring their reliability in the black-box setting where the system dynamics
are unknown. In this work, we consider the problems of certifying and repairing
neural network control policies and certificate functions in the black-box setting.
We propose a novel framework that utilizes runtime monitoring to detect system
behaviors that violate the property of interest under some initially trained neural
network policy and certificate. These violating behaviors are used to extract
new training data, that is used to re-train the neural network policy and the
certificate function and to ultimately repair them. We demonstrate the effectiveness
of our approach empirically by using it to repair and to boost the safety rate
of neural network policies learned by a state-of-the-art method for learning-based
control on two autonomous system control tasks.
acknowledgement: This work was supported in part by the ERC project ERC2020-AdG 101020093
article_processing_charge: No
arxiv: 1
author:
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Yu E, Zikelic D, Henzinger TA. Neural control and certificate repair via runtime
monitoring. In: Proceedings of the 39th AAAI Conference on Artificial Intelligence.
Vol 39. Association for the Advancement of Artificial Intelligence; 2025:26409-26417.
doi:10.1609/aaai.v39i25.34840'
apa: 'Yu, E., Zikelic, D., & Henzinger, T. A. (2025). Neural control and certificate
repair via runtime monitoring. In Proceedings of the 39th AAAI Conference on
Artificial Intelligence (Vol. 39, pp. 26409–26417). Philadelphia, PA, United
States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v39i25.34840'
chicago: Yu, Emily, Dorde Zikelic, and Thomas A Henzinger. “Neural Control and Certificate
Repair via Runtime Monitoring.” In Proceedings of the 39th AAAI Conference
on Artificial Intelligence, 39:26409–17. Association for the Advancement of
Artificial Intelligence, 2025. https://doi.org/10.1609/aaai.v39i25.34840.
ieee: E. Yu, D. Zikelic, and T. A. Henzinger, “Neural control and certificate repair
via runtime monitoring,” in Proceedings of the 39th AAAI Conference on Artificial
Intelligence, Philadelphia, PA, United States, 2025, vol. 39, no. 25, pp.
26409–26417.
ista: 'Yu E, Zikelic D, Henzinger TA. 2025. Neural control and certificate repair
via runtime monitoring. Proceedings of the 39th AAAI Conference on Artificial
Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 26409–26417.'
mla: Yu, Emily, et al. “Neural Control and Certificate Repair via Runtime Monitoring.”
Proceedings of the 39th AAAI Conference on Artificial Intelligence, vol.
39, no. 25, Association for the Advancement of Artificial Intelligence, 2025,
pp. 26409–17, doi:10.1609/aaai.v39i25.34840.
short: E. Yu, D. Zikelic, T.A. Henzinger, in:, Proceedings of the 39th AAAI Conference
on Artificial Intelligence, Association for the Advancement of Artificial Intelligence,
2025, pp. 26409–26417.
conference:
end_date: 2025-03-04
location: Philadelphia, PA, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2025-02-25
corr_author: '1'
date_created: 2025-05-11T22:02:40Z
date_published: 2025-04-11T00:00:00Z
date_updated: 2025-05-12T09:49:25Z
day: '11'
department:
- _id: ToHe
doi: 10.1609/aaai.v39i25.34840
ec_funded: 1
external_id:
arxiv:
- '2412.12996'
intvolume: ' 39'
issue: '25'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2412.12996
month: '04'
oa: 1
oa_version: Preprint
page: 26409-26417
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 39th AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: Neural control and certificate repair via runtime monitoring
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 39
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20189'
abstract:
- lang: eng
text: Certification was made mandatory for the first time in the latest hardware
model checking competition. In this case study, we investigate the trade-offs
of requiring certificates for both passing and failing properties in the competition.
Our evaluation shows that participating model checkers were able to produce compact,
correct certificates that could be verified with minimal overhead. Furthermore,
the certifying winner of the competition outperforms the previous non-certifying
state-of-the-art model checker, demonstrating that certification can be adopted
without compromising model checking efficiency.
acknowledgement: "This work is supported in part by the ERC-2020-AdG 101020093, the
LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland
under the project 336092, and a gift from Intel Corporation.\r\nFurthermore we of
course also owe a big thank-you to the submitters of model checkers and benchmarks
to the competition over all these years. Without their enthusiasm and support neither
the competition nor this study would exist."
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Nils
full_name: Froleyks, Nils
last_name: Froleyks
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
- first_name: Mathias
full_name: Preiner, Mathias
last_name: Preiner
- first_name: Armin
full_name: Biere, Armin
last_name: Biere
- first_name: Keijo
full_name: Heljanko, Keijo
last_name: Heljanko
citation:
ama: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates
to the hardware model checking competition. In: 37th International Conference
on Computer Aided Verification. Vol 15931. Springer Nature; 2025:281-295.
doi:10.1007/978-3-031-98668-0_14'
apa: 'Froleyks, N., Yu, E., Preiner, M., Biere, A., & Heljanko, K. (2025). Introducing
certificates to the hardware model checking competition. In 37th International
Conference on Computer Aided Verification (Vol. 15931, pp. 281–295). Zagreb,
Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-98668-0_14'
chicago: Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko.
“Introducing Certificates to the Hardware Model Checking Competition.” In 37th
International Conference on Computer Aided Verification, 15931:281–95. Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-98668-0_14.
ieee: N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates
to the hardware model checking competition,” in 37th International Conference
on Computer Aided Verification, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.
ista: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates
to the hardware model checking competition. 37th International Conference on Computer
Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.'
mla: Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking
Competition.” 37th International Conference on Computer Aided Verification,
vol. 15931, Springer Nature, 2025, pp. 281–95, doi:10.1007/978-3-031-98668-0_14.
short: N. Froleyks, E. Yu, M. Preiner, A. Biere, K. Heljanko, in:, 37th International
Conference on Computer Aided Verification, Springer Nature, 2025, pp. 281–295.
conference:
end_date: 2025-07-25
location: Zagreb, Croatia
name: 'CAV: Computer Aided Verification'
start_date: 2025-07-23
date_created: 2025-08-17T22:01:36Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2025-12-01T12:34:05Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-98668-0_14
ec_funded: 1
external_id:
isi:
- '001562507100014'
file:
- access_level: open_access
checksum: 15ec1bc9b9409d3b2736f4c9d5f42fd1
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T05:46:10Z
date_updated: 2025-09-02T05:46:10Z
file_id: '20266'
file_name: 2025_CAV_Froleyks.pdf
file_size: 1078274
relation: main_file
success: 1
file_date_updated: 2025-09-02T05:46:10Z
has_accepted_license: '1'
intvolume: ' 15931'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 281-295
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031986673'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Introducing certificates to the hardware model checking competition
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15931
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '20256'
abstract:
- lang: eng
text: We study the problem of predictive runtime monitoring of black-box dynamical
systems with quantitative safety properties. The black-box setting stipulates
that the exact semantics of the dynamical system and the controller are unknown,
and that we are only able to observe the state of the controlled (aka, closed-loop)
system at finitely many time points. We present a novel framework for predicting
future states of the system based on the states observed in the past. The numbers
of past states and of predicted future states are parameters provided by the user.
Our method is based on a combination of Taylor’s expansion and the backward difference
operator for numerical differentiation. We also derive an upper bound on the prediction
error under the assumption that the system dynamics and the controller are smooth.
The predicted states are then used to predict safety violations ahead in time.
Our experiments demonstrate practical applicability of our method for complex
black-box systems, showing that it is computationally lightweight and yet significantly
more accurate than the state-of-the-art predictive safety monitoring techniques.
acknowledgement: "This work was supported in part by the ERC project ERC-2020-AdG
101020093.\r\n"
alternative_title:
- PMLR
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: Fabian
full_name: Kresse, Fabian
id: faff3c84-23f6-11ef-9085-e5187b51c604
last_name: Kresse
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. Predictive monitoring of
black-box dynamical systems. In: 7th Annual Learning for Dynamics & Control
Conference. Vol 283. ML Research Press; 2025:804-816.'
apa: 'Henzinger, T. A., Kresse, F., Mallik, K., Yu, E., & Zikelic, D. (2025).
Predictive monitoring of black-box dynamical systems. In 7th Annual Learning
for Dynamics & Control Conference (Vol. 283, pp. 804–816). Ann Arbor,
MI, United States: ML Research Press.'
chicago: Henzinger, Thomas A, Fabian Kresse, Kaushik Mallik, Emily Yu, and Dorde
Zikelic. “Predictive Monitoring of Black-Box Dynamical Systems.” In 7th Annual
Learning for Dynamics & Control Conference, 283:804–16. ML Research Press,
2025.
ieee: T. A. Henzinger, F. Kresse, K. Mallik, E. Yu, and D. Zikelic, “Predictive
monitoring of black-box dynamical systems,” in 7th Annual Learning for Dynamics
& Control Conference, Ann Arbor, MI, United States, 2025, vol. 283, pp.
804–816.
ista: 'Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. 2025. Predictive monitoring
of black-box dynamical systems. 7th Annual Learning for Dynamics & Control
Conference. L4DC: Learning for Dynamics & Control, PMLR, vol. 283, 804–816.'
mla: Henzinger, Thomas A., et al. “Predictive Monitoring of Black-Box Dynamical
Systems.” 7th Annual Learning for Dynamics & Control Conference, vol.
283, ML Research Press, 2025, pp. 804–16.
short: T.A. Henzinger, F. Kresse, K. Mallik, E. Yu, D. Zikelic, in:, 7th Annual
Learning for Dynamics & Control Conference, ML Research Press, 2025, pp. 804–816.
conference:
end_date: 2025-06-06
location: Ann Arbor, MI, United States
name: 'L4DC: Learning for Dynamics & Control'
start_date: 2025-06-04
corr_author: '1'
date_created: 2025-08-31T22:01:32Z
date_published: 2025-06-01T00:00:00Z
date_updated: 2025-09-03T10:37:59Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: ChLa
ec_funded: 1
external_id:
arxiv:
- '2412.16564'
file:
- access_level: open_access
checksum: d5236e561560635f5ae1d17de4903033
content_type: application/pdf
creator: dernst
date_created: 2025-09-03T10:32:12Z
date_updated: 2025-09-03T10:32:12Z
file_id: '20283'
file_name: 2025_L4DC_HenzingerT.pdf
file_size: 489639
relation: main_file
success: 1
file_date_updated: 2025-09-03T10:32:12Z
has_accepted_license: '1'
intvolume: ' 283'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 804-816
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 7th Annual Learning for Dynamics & Control Conference
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Predictive monitoring of black-box dynamical systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 283
year: '2025'
...
---
OA_place: publisher
OA_type: diamond
_id: '20296'
abstract:
- lang: eng
text: Learning-based systems are increasingly deployed across various domains, yet
the complexity of traditional neural networks poses significant challenges for
formal verification. Unlike conventional neural networks, learned Logic Gate Networks
(LGNs) replace multiplications with Boolean logic gates, yielding a sparse, netlist-like
architecture that is inherently more amenable to symbolic verification, while
still delivering promising performance. In this paper, we introduce a SAT encoding
for verifying global robustness and fairness in LGNs. We evaluate our method on
five benchmark datasets, including a newly constructed 5-class variant, and find
that LGNs are both verification-friendly and maintain strong predictive performance.
acknowledged_ssus:
- _id: ScienComp
acknowledgement: "This work is supported in part by the ERC grant under Grant No.
ERC-2020-AdG 101020093 and\r\nthe Austrian Science Fund (FWF) [10.55776/COE12].
This research was supported by the Scientific\r\nService Units (SSU) of ISTA through
resources provided by Scientific Computing (SciComp)."
alternative_title:
- PMLR
article_number: '26'
article_processing_charge: No
arxiv: 1
author:
- first_name: Fabian
full_name: Kresse, Fabian
id: faff3c84-23f6-11ef-9085-e5187b51c604
last_name: Kresse
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
- first_name: Christoph
full_name: Lampert, Christoph
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Kresse F, Yu E, Lampert C, Henzinger TA. Logic gate neural networks are good
for verification. In: 2nd International Conferenceon Neuro-Symbolic Systems.
Vol 288. ML Research Press; 2025.'
apa: 'Kresse, F., Yu, E., Lampert, C., & Henzinger, T. A. (2025). Logic gate
neural networks are good for verification. In 2nd International Conferenceon
Neuro-Symbolic Systems (Vol. 288). Philadephia, PA, United States: ML Research
Press.'
chicago: Kresse, Fabian, Emily Yu, Christoph Lampert, and Thomas A Henzinger. “Logic
Gate Neural Networks Are Good for Verification.” In 2nd International Conferenceon
Neuro-Symbolic Systems, Vol. 288. ML Research Press, 2025.
ieee: F. Kresse, E. Yu, C. Lampert, and T. A. Henzinger, “Logic gate neural networks
are good for verification,” in 2nd International Conferenceon Neuro-Symbolic
Systems, Philadephia, PA, United States, 2025, vol. 288.
ista: 'Kresse F, Yu E, Lampert C, Henzinger TA. 2025. Logic gate neural networks
are good for verification. 2nd International Conferenceon Neuro-Symbolic Systems.
NeuS: International Conferenceon Neuro-Symbolic Systems, PMLR, vol. 288, 26.'
mla: Kresse, Fabian, et al. “Logic Gate Neural Networks Are Good for Verification.”
2nd International Conferenceon Neuro-Symbolic Systems, vol. 288, 26, ML
Research Press, 2025.
short: F. Kresse, E. Yu, C. Lampert, T.A. Henzinger, in:, 2nd International Conferenceon
Neuro-Symbolic Systems, ML Research Press, 2025.
conference:
end_date: 2025-05-30
location: Philadephia, PA, United States
name: 'NeuS: International Conferenceon Neuro-Symbolic Systems'
start_date: 2025-05-28
corr_author: '1'
date_created: 2025-09-07T22:01:34Z
date_published: 2025-06-01T00:00:00Z
date_updated: 2025-09-09T08:12:44Z
day: '01'
ddc:
- '000'
department:
- _id: ChLa
- _id: ToHe
ec_funded: 1
external_id:
arxiv:
- '2505.19932'
file:
- access_level: open_access
checksum: 90a32defed34787e771a5c1623b6b0d2
content_type: application/pdf
creator: dernst
date_created: 2025-09-09T08:10:13Z
date_updated: 2025-09-09T08:10:13Z
file_id: '20314'
file_name: 2025_NeuS_Kresse.pdf
file_size: 295466
relation: main_file
success: 1
file_date_updated: 2025-09-09T08:10:13Z
has_accepted_license: '1'
intvolume: ' 288'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 2nd International Conferenceon Neuro-Symbolic Systems
publication_identifier:
eissn:
- 2640-3498
publication_status: published
publisher: ML Research Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Logic gate neural networks are good for verification
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 288
year: '2025'
...
---
_id: '17413'
abstract:
- lang: eng
text: Certification helps to increase trust in formal verification of safety-critical
systems which require assurance on their correctness. In hardware model checking,
a widely used formal verification technique, phase abstraction is considered one
of the most commonly used preprocessing techniques. We present an approach to
certify an extended form of phase abstraction using a generic certificate format.
As in earlier works our approach involves constructing a witness circuit with
an inductive invariant property that certifies the correctness of the entire model
checking process, which is then validated by an independent certificate checker.
We have implemented and evaluated the proposed approach including certification
for various preprocessing configurations on hardware model checking competition
benchmarks. As an improvement on previous work in this area, the proposed method
is able to efficiently complete certification with an overhead of a fraction of
model checking time.
acknowledgement: This work is supported by the Austrian Science Fund (FWF) under the
project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG
101020093, the Academy of Finland under the project 336092 and by a gift from Intel
Corporation.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Nils
full_name: Froleyks, Nils
last_name: Froleyks
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
- first_name: Armin
full_name: Biere, Armin
last_name: Biere
- first_name: Keijo
full_name: Heljanko, Keijo
last_name: Heljanko
citation:
ama: 'Froleyks N, Yu E, Biere A, Heljanko K. Certifying phase abstraction. In: Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics). Vol 14739. Springer Nature; 2024:284-303.
doi:10.1007/978-3-031-63498-7_17'
apa: 'Froleyks, N., Yu, E., Biere, A., & Heljanko, K. (2024). Certifying phase
abstraction. In Lecture Notes in Computer Science (including subseries Lecture
Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol.
14739, pp. 284–303). Nancy, France: Springer Nature. https://doi.org/10.1007/978-3-031-63498-7_17'
chicago: Froleyks, Nils, Emily Yu, Armin Biere, and Keijo Heljanko. “Certifying
Phase Abstraction.” In Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
14739:284–303. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-63498-7_17.
ieee: N. Froleyks, E. Yu, A. Biere, and K. Heljanko, “Certifying phase abstraction,”
in Lecture Notes in Computer Science (including subseries Lecture Notes in
Artificial Intelligence and Lecture Notes in Bioinformatics), Nancy, France,
2024, vol. 14739, pp. 284–303.
ista: 'Froleyks N, Yu E, Biere A, Heljanko K. 2024. Certifying phase abstraction.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics). IJCAR: International Joint
Conference on Automated Reasoning, LNCS, vol. 14739, 284–303.'
mla: Froleyks, Nils, et al. “Certifying Phase Abstraction.” Lecture Notes in
Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), vol. 14739, Springer Nature, 2024, pp.
284–303, doi:10.1007/978-3-031-63498-7_17.
short: N. Froleyks, E. Yu, A. Biere, K. Heljanko, in:, Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics), Springer Nature, 2024, pp. 284–303.
conference:
end_date: 2024-07-06
location: Nancy, France
name: 'IJCAR: International Joint Conference on Automated Reasoning'
start_date: 2024-07-03
date_created: 2024-08-11T22:01:13Z
date_published: 2024-07-01T00:00:00Z
date_updated: 2025-09-08T08:49:53Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-63498-7_17
ec_funded: 1
external_id:
arxiv:
- '2405.04297'
isi:
- '001273489700017'
file:
- access_level: open_access
checksum: 7d7839fc8c5c680ea3ac09f40a66e55d
content_type: application/pdf
creator: dernst
date_created: 2024-08-12T06:53:39Z
date_updated: 2024-08-12T06:53:39Z
file_id: '17414'
file_name: 2024_LNCS_Froleyks.pdf
file_size: 556902
relation: main_file
success: 1
file_date_updated: 2024-08-12T06:53:39Z
has_accepted_license: '1'
intvolume: ' 14739'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 284-303
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031634970'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Certifying phase abstraction
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14739
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '17053'
abstract:
- lang: eng
text: We introduce a formalization of ternary simulation as abstract interpretation
along with a widening operator to speed up convergence. With the same goal, we
present a subsumption algorithm that can determine termination earlier than the
usual approach using hash sets. Additionally, we introduce a narrowing operator
that utilizes recent advances in backbone extraction, allowing to increase the
overapproximation precision in simulation at any time. The experiments evaluate
the presented techniques in the context of hardware model checking.
acknowledgement: This work is supported by the Austrian Science Fund (FWF) under the
project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG
101020093 and by a gift from Intel Corporation.
article_processing_charge: No
author:
- first_name: Nils
full_name: Froleyks, Nils
last_name: Froleyks
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
- first_name: Armin
full_name: Biere, Armin
last_name: Biere
citation:
ama: 'Froleyks N, Yu E, Biere A. Ternary simulation as abstract interpretation (Work
in Progress). In: 27th Workshop on Methods and Description Languages for Modeling
and Verification of Circuits and Systems. VDE Verlag; 2024:148-151.'
apa: 'Froleyks, N., Yu, E., & Biere, A. (2024). Ternary simulation as abstract
interpretation (Work in Progress). In 27th Workshop on Methods and Description
Languages for Modeling and Verification of Circuits and Systems (pp. 148–151).
Kaiserslautern, Germany: VDE Verlag.'
chicago: Froleyks, Nils, Emily Yu, and Armin Biere. “Ternary Simulation as Abstract
Interpretation (Work in Progress).” In 27th Workshop on Methods and Description
Languages for Modeling and Verification of Circuits and Systems, 148–51. VDE
Verlag, 2024.
ieee: N. Froleyks, E. Yu, and A. Biere, “Ternary simulation as abstract interpretation
(Work in Progress),” in 27th Workshop on Methods and Description Languages
for Modeling and Verification of Circuits and Systems, Kaiserslautern, Germany,
2024, pp. 148–151.
ista: 'Froleyks N, Yu E, Biere A. 2024. Ternary simulation as abstract interpretation
(Work in Progress). 27th Workshop on Methods and Description Languages for Modeling
and Verification of Circuits and Systems. MBMV: Methods and Description Languages
for Modeling and Verification of Circuits and Systems, 148–151.'
mla: Froleyks, Nils, et al. “Ternary Simulation as Abstract Interpretation (Work
in Progress).” 27th Workshop on Methods and Description Languages for Modeling
and Verification of Circuits and Systems, VDE Verlag, 2024, pp. 148–51.
short: N. Froleyks, E. Yu, A. Biere, in:, 27th Workshop on Methods and Description
Languages for Modeling and Verification of Circuits and Systems, VDE Verlag, 2024,
pp. 148–151.
conference:
end_date: 2024-02-15
location: Kaiserslautern, Germany
name: 'MBMV: Methods and Description Languages for Modeling and Verification of
Circuits and Systems'
start_date: 2024-02-14
das_tickbox: '1'
date_created: 2024-05-26T22:00:58Z
date_published: 2024-02-01T00:00:00Z
date_updated: 2026-07-07T07:03:23Z
day: '01'
department:
- _id: ToHe
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://cca.informatik.uni-freiburg.de/papers/FroleyksYuBiere-MBMV24.pdf
month: '02'
oa: 1
oa_version: Submitted Version
page: 148-151
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 27th Workshop on Methods and Description Languages for Modeling and Verification
of Circuits and Systems
publication_identifier:
isbn:
- '9783800762682'
publication_status: published
publisher: VDE Verlag
quality_controlled: '1'
scopus_import: '1'
status: public
title: Ternary simulation as abstract interpretation (Work in Progress)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2024'
...