---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '21012'
abstract:
- lang: eng
text: In certifiable machine learning, AI systems produce not only results but also
verifiable certificates that the results can be trusted.
acknowledgement: T.A.H. thanks Đorde Žikelic for many stimulating discussions about
CML. This work was supported in part by NSFCPS Frontier Grant 1545126, by a BAIR
Commons project, by the Berkeley iCy-Phy Center, by the Stanford Center for Automated
Reasoning, and by the ERC Advanced Grant 101020093.
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Clark
full_name: Barrett, Clark
last_name: Barrett
- 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: Sanjit A.
full_name: Seshia, Sanjit A.
last_name: Seshia
citation:
ama: 'Barrett C, Henzinger TA, Seshia SA. Certificates in AI: Learn but verify.
Communications of the ACM. 2026;69(1):66-75. doi:10.1145/3737447'
apa: 'Barrett, C., Henzinger, T. A., & Seshia, S. A. (2026). Certificates in
AI: Learn but verify. Communications of the ACM. Association for Computing
Machinery. https://doi.org/10.1145/3737447'
chicago: 'Barrett, Clark, Thomas A Henzinger, and Sanjit A. Seshia. “Certificates
in AI: Learn but Verify.” Communications of the ACM. Association for Computing
Machinery, 2026. https://doi.org/10.1145/3737447.'
ieee: 'C. Barrett, T. A. Henzinger, and S. A. Seshia, “Certificates in AI: Learn
but verify,” Communications of the ACM, vol. 69, no. 1. Association for
Computing Machinery, pp. 66–75, 2026.'
ista: 'Barrett C, Henzinger TA, Seshia SA. 2026. Certificates in AI: Learn but verify.
Communications of the ACM. 69(1), 66–75.'
mla: 'Barrett, Clark, et al. “Certificates in AI: Learn but Verify.” Communications
of the ACM, vol. 69, no. 1, Association for Computing Machinery, 2026, pp.
66–75, doi:10.1145/3737447.'
short: C. Barrett, T.A. Henzinger, S.A. Seshia, Communications of the ACM 69 (2026)
66–75.
corr_author: '1'
date_created: 2026-01-20T10:08:21Z
date_published: 2026-01-01T00:00:00Z
date_updated: 2026-01-21T08:55:24Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3737447
ec_funded: 1
file:
- access_level: open_access
checksum: d909a9091c254b2d18ba014124663f69
content_type: application/pdf
creator: dernst
date_created: 2026-01-21T08:52:07Z
date_updated: 2026-01-21T08:52:07Z
file_id: '21028'
file_name: 2026_CommACM_Barrett.pdf
file_size: 2623108
relation: main_file
success: 1
file_date_updated: 2026-01-21T08:52:07Z
has_accepted_license: '1'
intvolume: ' 69'
issue: '1'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '01'
oa: 1
oa_version: Published Version
page: 66-75
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Communications of the ACM
publication_identifier:
eissn:
- 1557-7317
issn:
- 0001-0782
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Certificates in AI: Learn but verify'
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 69
year: '2026'
...
---
OA_place: repository
_id: '21401'
abstract:
- lang: eng
text: "Runtime verification offers scalable solutions to improve the safety and
reliability of systems. However, systems that require verification or monitoring
by a third party to ensure compliance with a specification might contain sensitive
information, causing privacy concerns when usual runtime verification approaches
are used. Privacy is compromised if protected information about the system, or
sensitive data that is processed by the system, is revealed. In addition, revealing
the specification being monitored may undermine the essence of third-party verification.\r\n\r\nIn
this thesis, we propose a protocol for privacy-preserving runtime verification
of systems against formal sequential specifications. We develop the protocol in
two steps. In the first step, the monitor verifies whether the system satisfies
the specification without learning anything else, though both parties are aware
of the specification. In the second step, we extend the protocol to ensure that
the system remains oblivious to the monitored specification, while the monitor
learns only whether the system satisfies the specification and nothing more. Our
protocol adapts and improves existing techniques used in cryptography, and more
specifically, multi-party computation.\r\n\r\nThe sequential specification defines
the observation step of the monitor, whose granularity depends on the situation
(e.g., banks may be monitored on a daily basis). Our protocol exchanges a single
message per observation step, after an initialization phase. This design minimizes
communication overhead, enabling relatively lightweight privacy-preserving monitoring.
We implement our approach for monitoring specifications described by register
automata and evaluate it experimentally.\r\n"
acknowledgement: "This work is part of the project VAMOS, which has received funding
from the European\r\nResearch Council (ERC) under grant agreement No. 101020093,
and the Austrian Science\r\nFund (FWF) SFB project SpyCoDe F8502.\r\n"
alternative_title:
- ISTA Master’s Thesis
article_processing_charge: No
author:
- first_name: Mahyar
full_name: Karimi, Mahyar
id: 6e5417ba-5355-11ee-ae5a-94c2e510b26b
last_name: Karimi
orcid: 0009-0005-0820-1696
citation:
ama: Karimi M. Privacy-preserving runtime verification. 2026. doi:10.15479/AT-ISTA-21401
apa: Karimi, M. (2026). Privacy-preserving runtime verification. Institute
of Science and Technology Austria. https://doi.org/10.15479/AT-ISTA-21401
chicago: Karimi, Mahyar. “Privacy-Preserving Runtime Verification.” Institute of
Science and Technology Austria, 2026. https://doi.org/10.15479/AT-ISTA-21401.
ieee: M. Karimi, “Privacy-preserving runtime verification,” Institute of Science
and Technology Austria, 2026.
ista: Karimi M. 2026. Privacy-preserving runtime verification. Institute of Science
and Technology Austria.
mla: Karimi, Mahyar. Privacy-Preserving Runtime Verification. Institute of
Science and Technology Austria, 2026, doi:10.15479/AT-ISTA-21401.
short: M. Karimi, Privacy-Preserving Runtime Verification, Institute of Science
and Technology Austria, 2026.
corr_author: '1'
date_created: 2026-03-05T15:20:47Z
date_published: 2026-03-05T00:00:00Z
date_updated: 2026-03-13T13:37:20Z
day: '05'
ddc:
- '000'
degree_awarded: MS
department:
- _id: GradSch
- _id: ToHe
doi: 10.15479/AT-ISTA-21401
ec_funded: 1
file:
- access_level: open_access
checksum: 3f49f05c9d123e14d7adb73d3bc50fe2
content_type: application/pdf
creator: mkarimi
date_created: 2026-03-06T14:06:25Z
date_updated: 2026-03-10T15:20:09Z
file_id: '21404'
file_name: 2026_Karimi_Mahyar_Thesis.pdf
file_size: 766048
relation: main_file
- access_level: closed
checksum: 8fb9db4b4187e26443369a993427a5ff
content_type: application/zip
creator: mkarimi
date_created: 2026-03-06T14:06:25Z
date_updated: 2026-03-06T14:06:25Z
file_id: '21405'
file_name: 2026_Karimi_Mahyar_Thesis_src.zip
file_size: 1243394
relation: source_file
file_date_updated: 2026-03-10T15:20:09Z
has_accepted_license: '1'
keyword:
- Privacy-preserving verification
- Runtime verification
- Monitoring
- Reactive functionalities
- Cryptographic protocols
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: '60'
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 34a4ce89-11ca-11ed-8bc3-8cc37fb6e11f
grant_number: F8512
name: Security and Privacy by Design for Complex Systems
publication_identifier:
issn:
- 2791-4585
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '21020'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Privacy-preserving runtime verification
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2026'
...
---
OA_place: publisher
OA_type: hybrid
_id: '18169'
abstract:
- lang: eng
text: "As the complexity and criticality of software increase every year, so does
the importance of runtime monitoring. Third-party and best-effort monitoring are
especially valuable, yet under-explored areas of runtime monitoring. In this context,
third-party monitoring means monitoring with a limited knowledge of the monitored
software (as it has been developed by a third party). Best-effort monitoring keeps
pace with the monitored software at the cost of possibly imprecise verdicts when
keeping up with the monitored software would not be feasible. Most existing monitoring
frameworks do not support the combination of third-party and best-effort monitoring
because they either require the full access to the monitored code or the ability
to process all observable events, or both.\r\nWe present a middleware framework,
Vamos, for the runtime monitoring of software. Vamos is explicitly designed to
support third-party and best-effort scenarios. The design goals of Vamos are (i)
efficiency (tracing events with low overhead), (ii) flexibility (the ability to
monitor a variety of different event channels, and to connect to a wide range
of monitors), and (iii) ease-of-use. To achieve its goals, Vamos combines aspects
of event broker and event recognition systems with aspects of stream processing
systems.\r\nWe implemented a prototype toolchain for Vamos and conducted a set
of experiments demonstrating the usability of the scheme. The results indicate
that Vamos enables writing useful yet efficient monitors, and simplifies key aspects
of setting up a monitoring system from scratch."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The
authors would like to thank the STTT reviewers for their valuable feedback and suggestions.
article_number: '103212'
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- 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: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. VAMOS: Middleware for best-effort
third-party monitoring. Science of Computer Programming. 2025;240(2). doi:10.1016/j.scico.2024.103212'
apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2025).
VAMOS: Middleware for best-effort third-party monitoring. Science of Computer
Programming. Elsevier. https://doi.org/10.1016/j.scico.2024.103212'
chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger.
“VAMOS: Middleware for Best-Effort Third-Party Monitoring.” Science of Computer
Programming. Elsevier, 2025. https://doi.org/10.1016/j.scico.2024.103212.'
ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “VAMOS: Middleware
for best-effort third-party monitoring,” Science of Computer Programming,
vol. 240, no. 2. Elsevier, 2025.'
ista: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2025. VAMOS: Middleware
for best-effort third-party monitoring. Science of Computer Programming. 240(2),
103212.'
mla: 'Chalupa, Marek, et al. “VAMOS: Middleware for Best-Effort Third-Party Monitoring.”
Science of Computer Programming, vol. 240, no. 2, 103212, Elsevier, 2025,
doi:10.1016/j.scico.2024.103212.'
short: M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, Science of Computer
Programming 240 (2025).
corr_author: '1'
date_created: 2024-10-06T22:01:10Z
date_published: 2025-02-01T00:00:00Z
date_updated: 2025-09-09T12:25:29Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.scico.2024.103212
ec_funded: 1
external_id:
isi:
- '001327852600001'
file:
- access_level: open_access
checksum: cd93c0c356e479ffccfbe8499b6ba8e2
content_type: application/pdf
creator: dernst
date_created: 2025-01-13T09:02:47Z
date_updated: 2025-01-13T09:02:47Z
file_id: '18831'
file_name: 2024_ScienceCompProg_Chalupa.pdf
file_size: 1173677
relation: main_file
success: 1
file_date_updated: 2025-01-13T09:02:47Z
has_accepted_license: '1'
intvolume: ' 240'
isi: 1
issue: '2'
language:
- iso: eng
month: '02'
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: Science of Computer Programming
publication_identifier:
issn:
- 0167-6423
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '12856'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: 'VAMOS: Middleware for best-effort third-party monitoring'
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 240
year: '2025'
...
---
DOAJ_listed: '1'
OA_place: publisher
OA_type: gold
_id: '19796'
abstract:
- lang: eng
text: "Motivation: Boolean networks are popular dynamical models of cellular processes
in systems biology. Their attractors model phenotypes that arise from the interplay
of key regulatory subcircuits. A succession diagram (SD) describes this interplay
in a discrete analog of Waddington’s epigenetic attractor landscape that allows
for fast identification of attractors and attractor control strategies. Efficient
computational tools for studying SDs are essential for the understanding of Boolean
attractor landscapes and connecting them to their biological functions.\r\nResults:
We present a new approach to SD construction for asynchronously updated Boolean
networks, implemented in the biologist’s Boolean attractor landscape mapper, biobalm.
We compare biobalm to similar tools and find a substantial performance increase
in SD construction, attractor identification, and attractor control. We perform
the most comprehensive comparative analysis to date of the SD structure in experimentally-validated
Boolean models of cell processes and random ensembles. We find that random models
(including critical Kauffman networks) have relatively small SDs, indicating simple
decision structures. In contrast, nonrandom models from the literature are enriched
in extremely large SDs, indicating an abundance of decision points and suggesting
the presence of complex Waddington landscapes in nature.\r\nAvailability and implementation:
The tool biobalm is available online at https://github.com/jcrozum/biobalm. Further
data, scripts for testing, analysis, and figure generation are available online
at https://github.com/jcrozum/biobalm-analysis and in the reproducibility artefact
at https://doi.org/10.5281/zenodo.13854760."
acknowledgement: V.-G.T. was supported by Institut Carnot STAR, Marseille, France.
K.H.P. was supported by NSF grant MCB1715826 to Réka Albert. S.P. has received funding
from the European Union’s Horizon 2020 Research and Innovation Programme under the
Marie Sklodowska-Curie Grant Agreement No. 101034413. J.C.R. was supported by internal
departmental funds provided by Luis M. Rocha. No funding bodies had any role in
study design, analysis, decision to publish, or preparation of the article.
article_number: btaf280
article_processing_charge: Yes
article_type: original
author:
- first_name: Van Giang
full_name: Trinh, Van Giang
last_name: Trinh
- first_name: Kyu Hyong
full_name: Park, Kyu Hyong
last_name: Park
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: Jordan C.
full_name: Rozum, Jordan C.
last_name: Rozum
citation:
ama: Trinh VG, Park KH, Pastva S, Rozum JC. Mapping the attractor landscape of Boolean
networks with biobalm. Bioinformatics. 2025;41(5). doi:10.1093/bioinformatics/btaf280
apa: Trinh, V. G., Park, K. H., Pastva, S., & Rozum, J. C. (2025). Mapping the
attractor landscape of Boolean networks with biobalm. Bioinformatics. Oxford
University Press. https://doi.org/10.1093/bioinformatics/btaf280
chicago: Trinh, Van Giang, Kyu Hyong Park, Samuel Pastva, and Jordan C. Rozum. “Mapping
the Attractor Landscape of Boolean Networks with Biobalm.” Bioinformatics.
Oxford University Press, 2025. https://doi.org/10.1093/bioinformatics/btaf280.
ieee: V. G. Trinh, K. H. Park, S. Pastva, and J. C. Rozum, “Mapping the attractor
landscape of Boolean networks with biobalm,” Bioinformatics, vol. 41, no.
5. Oxford University Press, 2025.
ista: Trinh VG, Park KH, Pastva S, Rozum JC. 2025. Mapping the attractor landscape
of Boolean networks with biobalm. Bioinformatics. 41(5), btaf280.
mla: Trinh, Van Giang, et al. “Mapping the Attractor Landscape of Boolean Networks
with Biobalm.” Bioinformatics, vol. 41, no. 5, btaf280, Oxford University
Press, 2025, doi:10.1093/bioinformatics/btaf280.
short: V.G. Trinh, K.H. Park, S. Pastva, J.C. Rozum, Bioinformatics 41 (2025).
corr_author: '1'
date_created: 2025-06-08T22:01:22Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-09-30T12:46:33Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1093/bioinformatics/btaf280
ec_funded: 1
external_id:
isi:
- '001493400600001'
pmid:
- '40327535'
file:
- access_level: open_access
checksum: fa9d68aa0f5ce37598a623c9be936f09
content_type: application/pdf
creator: dernst
date_created: 2025-06-10T07:07:45Z
date_updated: 2025-06-10T07:07:45Z
file_id: '19801'
file_name: 2025_Bioinformatics_Trinh.pdf
file_size: 2695801
relation: main_file
success: 1
file_date_updated: 2025-06-10T07:07:45Z
has_accepted_license: '1'
intvolume: ' 41'
isi: 1
issue: '5'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Bioinformatics
publication_identifier:
eissn:
- 1367-4811
publication_status: published
publisher: Oxford University Press
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/jcrozum/biobalm
record:
- id: '19800'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Mapping the attractor landscape of Boolean networks with biobalm
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: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 41
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19854'
abstract:
- lang: eng
text: 'Asynchronous Boolean networks are a type of discrete dynamical system in
which each variable can take one of two states, and a single variable state is
updated in each time step according to pre-selected rules. Boolean networks are
popular in systems biology due to their ability to model long-term biological
phenotypes within a qualitative, predictive framework. Boolean networks model
phenotypes as attractors, which are closely linked to minimal trap spaces (inescapable
hypercubes in the system’s state space). In biological applications, attractors
and minimal trap spaces are typically in one-to-one correspondence. However, this
correspondence is not guaranteed: motif-avoidant attractors (MAAs) that lie outside
minimal trap spaces are possible. MAAs are rare and poorly understood, despite
recent efforts. In this contribution to the BMB & JMB Special Collection “Problems,
Progress and Perspectives in Mathematical and Computational Biology”, we summarize
the current state of knowledge regarding MAAs and present several novel observations
regarding their response to node deletion reductions and linear extensions of
edges. We conduct large-scale computational studies on an ensemble of 14 000 models
derived from published Boolean models of biological systems, and more than 100
million Random Boolean Networks. Our findings quantify the rarity of MAAs; in
particular, we only observed MAAs in biological models after applying standard
simplification methods, highlighting the role of network reduction in introducing
MAAs into the dynamics. We also show that MAAs are fragile to linear extensions:
in sparse networks, even a single linear node can disrupt virtually all MAAs.
Motivated by this observation, we improve the upper bound on the number of delays
needed to disrupt a motif-avoidant attractor.'
acknowledgement: Ondřej Huvar has been supported by the Czech Science Foundation grant
No. GA22-10845S. Samuel Pastva received funding from the European Union’s Horizon
2020 research and innovation programme under the Marie Sklodowska-Curie Grant Agreement
No. 101034413. Kyu Hyong Park and Réka Albert have been supported by NSF grant MCB
1715826 and ARO grant 79961-SM-MUR. No funding bodies had any role in study design,
analysis, decision to publish, or preparation of the manuscript.
article_number: '11'
article_processing_charge: Yes (in subscription journal)
article_type: original
arxiv: 1
author:
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: Kyu Hyong
full_name: Park, Kyu Hyong
last_name: Park
- first_name: Ondřej
full_name: Huvar, Ondřej
last_name: Huvar
- first_name: Jordan C.
full_name: Rozum, Jordan C.
last_name: Rozum
- first_name: Réka
full_name: Albert, Réka
last_name: Albert
citation:
ama: 'Pastva S, Park KH, Huvar O, Rozum JC, Albert R. An open problem: Why are motif-avoidant
attractors so rare in asynchronous Boolean networks? Journal of Mathematical
Biology. 2025;91. doi:10.1007/s00285-025-02235-8'
apa: 'Pastva, S., Park, K. H., Huvar, O., Rozum, J. C., & Albert, R. (2025).
An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean
networks? Journal of Mathematical Biology. Springer Nature. https://doi.org/10.1007/s00285-025-02235-8'
chicago: 'Pastva, Samuel, Kyu Hyong Park, Ondřej Huvar, Jordan C. Rozum, and Réka
Albert. “An Open Problem: Why Are Motif-Avoidant Attractors so Rare in Asynchronous
Boolean Networks?” Journal of Mathematical Biology. Springer Nature, 2025.
https://doi.org/10.1007/s00285-025-02235-8.'
ieee: 'S. Pastva, K. H. Park, O. Huvar, J. C. Rozum, and R. Albert, “An open problem:
Why are motif-avoidant attractors so rare in asynchronous Boolean networks?,”
Journal of Mathematical Biology, vol. 91. Springer Nature, 2025.'
ista: 'Pastva S, Park KH, Huvar O, Rozum JC, Albert R. 2025. An open problem: Why
are motif-avoidant attractors so rare in asynchronous Boolean networks? Journal
of Mathematical Biology. 91, 11.'
mla: 'Pastva, Samuel, et al. “An Open Problem: Why Are Motif-Avoidant Attractors
so Rare in Asynchronous Boolean Networks?” Journal of Mathematical Biology,
vol. 91, 11, Springer Nature, 2025, doi:10.1007/s00285-025-02235-8.'
short: S. Pastva, K.H. Park, O. Huvar, J.C. Rozum, R. Albert, Journal of Mathematical
Biology 91 (2025).
corr_author: '1'
date_created: 2025-06-22T22:02:05Z
date_published: 2025-06-12T00:00:00Z
date_updated: 2025-09-30T13:36:46Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00285-025-02235-8
ec_funded: 1
external_id:
arxiv:
- '2410.03976'
isi:
- '001507009300001'
file:
- access_level: open_access
checksum: a385ef2662f1d0c3497ed3f2721fe594
content_type: application/pdf
creator: dernst
date_created: 2025-06-23T11:10:01Z
date_updated: 2025-06-23T11:10:01Z
file_id: '19871'
file_name: 2025_JourMathBiology_Pastva.pdf
file_size: 1243163
relation: main_file
success: 1
file_date_updated: 2025-06-23T11:10:01Z
has_accepted_license: '1'
intvolume: ' 91'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Journal of Mathematical Biology
publication_identifier:
eissn:
- 1432-1416
issn:
- 0303-6812
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'An open problem: Why are motif-avoidant attractors so rare in asynchronous
Boolean networks?'
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: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 91
year: '2025'
...
---
OA_type: closed access
_id: '20024'
abstract:
- lang: eng
text: 'Cooperative software verification divides the task of software verification
among several verification tools in order to increase efficiency and effectiveness.
The basic approach is to let verifiers work on different parts of a program and
at the end join verification results. While this idea is intuitively appealing,
cooperative verification is usually hindered by the fact that program decomposition
(1) is often static, disregarding strengths and weaknesses of employed verifiers,
and (2) often represents the decomposed program parts in a specific proprietary
format, thereby making the use of off-the-shelf verifiers in cooperative verification
difficult. In this paper, we propose a novel cooperative verification scheme that
we call dynamic program splitting (DPS). Splitting decomposes programs into (smaller)
programs, and thus directly enables the use of off-the-shelf tools. In DPS, splitting
is dynamically applied on demand: Verification starts by giving a verification
task (a program plus a correctness specification) to a verifier V1. Whenever V1
finds the current task to be hard to verify, it splits the task (i.e., the program)
and restarts verification on subtasks. DPS continues until (1) a violation is
found, (2) all subtasks are completed or (3) some user-defined stopping criterion
is met. In the latter case, the remaining uncompleted subtasks are merged into
a single one and are given to a next verifier V2, repeating the same procedure
on the still unverified program parts. This way, the decomposition is steered
by what is hard to verify for particular verifiers, leveraging their complementary
strengths. We have implemented dynamic program splitting and evaluated it on benchmarks
of the annual software verification competition SV-COMP. The evaluation shows
that cooperative verification with DPS is able to solve verification tasks that
none of the constituent verifiers can solve, without any significant overhead.'
acknowledgement: This work is partially supported by the German Research Foundation
(DFG) – WE2290/13-2 (Coop2), and in part by the ERC-2020-AdG 101020093.
article_processing_charge: No
author:
- first_name: Cedric
full_name: Richter, Cedric
last_name: Richter
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Heike
full_name: Wehrheim, Heike
last_name: Wehrheim
citation:
ama: 'Richter C, Chalupa M, Jakobs M-C, Wehrheim H. Cooperative software verification
via dynamic program splitting. In: 47th International Conference on Software
Engineering. IEEE; 2025:2087-2099. doi:10.1109/ICSE55347.2025.00092'
apa: 'Richter, C., Chalupa, M., Jakobs, M.-C., & Wehrheim, H. (2025). Cooperative
software verification via dynamic program splitting. In 47th International
Conference on Software Engineering (pp. 2087–2099). Ottawa, ON, Canada: IEEE.
https://doi.org/10.1109/ICSE55347.2025.00092'
chicago: Richter, Cedric, Marek Chalupa, Marie-Christine Jakobs, and Heike Wehrheim.
“Cooperative Software Verification via Dynamic Program Splitting.” In 47th
International Conference on Software Engineering, 2087–99. IEEE, 2025. https://doi.org/10.1109/ICSE55347.2025.00092.
ieee: C. Richter, M. Chalupa, M.-C. Jakobs, and H. Wehrheim, “Cooperative software
verification via dynamic program splitting,” in 47th International Conference
on Software Engineering, Ottawa, ON, Canada, 2025, pp. 2087–2099.
ista: 'Richter C, Chalupa M, Jakobs M-C, Wehrheim H. 2025. Cooperative software
verification via dynamic program splitting. 47th International Conference on Software
Engineering. ICSE: International Conference on Software Engineering, 2087–2099.'
mla: Richter, Cedric, et al. “Cooperative Software Verification via Dynamic Program
Splitting.” 47th International Conference on Software Engineering, IEEE,
2025, pp. 2087–99, doi:10.1109/ICSE55347.2025.00092.
short: C. Richter, M. Chalupa, M.-C. Jakobs, H. Wehrheim, in:, 47th International
Conference on Software Engineering, IEEE, 2025, pp. 2087–2099.
conference:
end_date: 2025-05-06
location: Ottawa, ON, Canada
name: 'ICSE: International Conference on Software Engineering'
start_date: 2025-04-26
corr_author: '1'
date_created: 2025-07-16T11:32:29Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-09-30T14:01:55Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/ICSE55347.2025.00092
ec_funded: 1
external_id:
isi:
- '001538318100163'
isi: 1
language:
- iso: eng
month: '05'
oa_version: None
page: 2087-2099
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 47th International Conference on Software Engineering
publication_identifier:
eissn:
- 1558-1225
isbn:
- '9798331505691'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Cooperative software verification via dynamic program splitting
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '20186'
abstract:
- lang: eng
text: Enforcement of information-flow policies has been extensively studied by language-based
approaches over the past few decades. In this paper, we propose an alternative,
novel, general, and effective approach using enforcement of hyperproperties– a
powerful formalism for expressing and reasoning about a wide range of information-flow
security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties
expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer
has null, some, or complete information about the implementation of the system
under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce
the problem to controller synthesis for hyperproperties and subsequently to the
satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers
are transferable with low-overhead. We conduct a rich set of case studies, including
information-flow control for JavaScript code, as well as synthesizing obfuscators
for control plants.
acknowledgement: This project was funded in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe F8502, Vienna Science and Technology Fund (WWTF) [10.47379/ICT19018]
(ProbInG) and WWTF project ICT22-023 (TAIGER), National Science Foundation (NSF)
CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114. Open access
funding provided by Institute of Science and Technology (IST Austria).
article_number: '30'
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Tzu Han
full_name: Hsu, Tzu Han
last_name: Hsu
- first_name: Ana A
full_name: Oliveira Da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira Da Costa
- first_name: Andrew
full_name: Wintenberg, Andrew
last_name: Wintenberg
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Borzoo
full_name: Bonakdarpour, Borzoo
last_name: Bonakdarpour
citation:
ama: Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box
runtime enforcement of hyperproperties. Acta Informatica. 2025;62(3). doi:10.1007/s00236-025-00502-1
apa: Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., & Bonakdarpour,
B. (2025). Gray-box runtime enforcement of hyperproperties. Acta Informatica.
Springer Nature. https://doi.org/10.1007/s00236-025-00502-1
chicago: Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci,
and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” Acta
Informatica. Springer Nature, 2025. https://doi.org/10.1007/s00236-025-00502-1.
ieee: T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour,
“Gray-box runtime enforcement of hyperproperties,” Acta Informatica, vol.
62, no. 3. Springer Nature, 2025.
ista: Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. 2025.
Gray-box runtime enforcement of hyperproperties. Acta Informatica. 62(3), 30.
mla: Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” Acta
Informatica, vol. 62, no. 3, 30, Springer Nature, 2025, doi:10.1007/s00236-025-00502-1.
short: T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour,
Acta Informatica 62 (2025).
corr_author: '1'
date_created: 2025-08-17T22:01:36Z
date_published: 2025-09-01T00:00:00Z
date_updated: 2025-09-30T14:20:11Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00236-025-00502-1
external_id:
isi:
- '001546115300001'
file:
- access_level: open_access
checksum: 90a43350fd4a8c5cb5b1b0e1aea7970d
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T05:53:47Z
date_updated: 2025-09-02T05:53:47Z
file_id: '20267'
file_name: 2025_ActaInformatica_Hsu.pdf
file_size: 6505049
relation: main_file
success: 1
file_date_updated: 2025-09-02T05:53:47Z
has_accepted_license: '1'
intvolume: ' 62'
isi: 1
issue: '3'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Gray-box runtime enforcement of hyperproperties
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: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 62
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: hybrid
_id: '20225'
abstract:
- lang: eng
text: "We present the first supermartingale certificate for quantitative \r\n-regular
properties of discrete-time infinite-state stochastic systems. Our certificate
is defined on the product of the stochastic system and a limit-deterministic Büchi
automaton that specifies the property of interest; hence we call it a limit-deterministic
Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied
only to quantitative reachability, safety, or reach-avoid properties, and to qualitative
(i.e., probability 1) \r\n-regular properties.We also present fully automated
algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic
system dynamics and the controller can be represented in terms of polynomial inequalities.
Our experiments demonstrate the ability of our method to solve verification and
control tasks for stochastic systems that were beyond the reach of previous supermartingale-based
approaches."
acknowledgement: This work was supported in part by the Singapore Ministry of Education
(MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SIS-SMU-100) and
the ERC project ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
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: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Pouya
full_name: Sadeghi, Pouya
last_name: Sadeghi
- 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, Mallik K, Sadeghi P, Zikelic D. Supermartingale certificates
for quantitative omega-regular verification and control. In: 37th International
Conference on Computer Aided Verification. Vol 15932. Springer Nature; 2025:29-55.
doi:10.1007/978-3-031-98679-6_2'
apa: 'Henzinger, T. A., Mallik, K., Sadeghi, P., & Zikelic, D. (2025). Supermartingale
certificates for quantitative omega-regular verification and control. In 37th
International Conference on Computer Aided Verification (Vol. 15932, pp. 29–55).
Zagreb, Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-98679-6_2'
chicago: Henzinger, Thomas A, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic.
“Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.”
In 37th International Conference on Computer Aided Verification, 15932:29–55.
Springer Nature, 2025. https://doi.org/10.1007/978-3-031-98679-6_2.
ieee: T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates
for quantitative omega-regular verification and control,” in 37th International
Conference on Computer Aided Verification, Zagreb, Croatia, 2025, vol. 15932,
pp. 29–55.
ista: 'Henzinger TA, Mallik K, Sadeghi P, Zikelic D. 2025. Supermartingale certificates
for quantitative omega-regular verification and control. 37th International Conference
on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15932,
29–55.'
mla: Henzinger, Thomas A., et al. “Supermartingale Certificates for Quantitative
Omega-Regular Verification and Control.” 37th International Conference on Computer
Aided Verification, vol. 15932, Springer Nature, 2025, pp. 29–55, doi:10.1007/978-3-031-98679-6_2.
short: T.A. Henzinger, K. Mallik, P. Sadeghi, D. Zikelic, in:, 37th International
Conference on Computer Aided Verification, Springer Nature, 2025, pp. 29–55.
conference:
end_date: 2025-07-25
location: Zagreb, Croatia
name: 'CAV: Computer Aided Verification'
start_date: 2025-07-23
date_created: 2025-08-24T22:01:31Z
date_published: 2025-07-22T00:00:00Z
date_updated: 2025-12-01T12:34:41Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-98679-6_2
ec_funded: 1
external_id:
arxiv:
- '2505.18833'
isi:
- '001562506600002'
file:
- access_level: open_access
checksum: beb1e2637de5b2268cc2262119439113
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T07:34:33Z
date_updated: 2025-09-02T07:34:33Z
file_id: '20272'
file_name: 2025_CAV_HenzingerT.pdf
file_size: 884831
relation: main_file
success: 1
file_date_updated: 2025-09-02T07:34:33Z
has_accepted_license: '1'
intvolume: ' 15932'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 29-55
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:
- '9783031986789'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Supermartingale certificates for quantitative omega-regular verification and control
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: 15932
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '20253'
abstract:
- lang: eng
text: "A quantitative word automaton (QWA) defines a function from infinite words
to values. For example, every infinite run of a limit-average QWA \U0001D49C obtains
a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained
by nondeterministic runs of \U0001D49C over w. We introduce quantitative language
automata (QLAs) that define functions from language generators (i.e., implementations)
to values, where a language generator can be nonprobabilistic, defining a set
of infinite words, or probabilistic, defining a probability measure over infinite
words. A QLA consists of a QWA and an aggregator function. For example, given
a QWA \U0001D49C, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest
lower bound assigned by \U0001D49C to any word in L. For boolean value sets, QWAs
define boolean properties of traces, and QLAs define boolean properties of sets
of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a
specification language for a generalization of hyperproperties, called quantitative
hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty
assigns a value to each set (resp. distribution) G of traces, e.g., the minimal
(resp. expected) average response time exhibited by the traces in G. We give several
examples of quantitative hyperproperties and investigate three paradigmatic problems
for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem,
given a QLA \U0001D538 and an implementation G, we ask for the value that \U0001D538
assigns to G. In the nonemptiness (resp. universality) problem, given a QLA \U0001D538
and a value k, we ask whether \U0001D538 assigns at least k to some (resp. every)
language. We provide a comprehensive picture of decidability for these problems
for QLAs with common aggregators as well as their restrictions to ω-regular languages
and trace distributions generated by finite-state Markov chains."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LIPIcs
article_number: '21'
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: Pavol
full_name: Kebis, Pavol
id: 2e0132b3-4e98-11ef-b275-cf7281c2802a
last_name: Kebis
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Quantitative language automata.
In: 36th International Conference on Concurrency Theory. Vol 348. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:10.4230/LIPIcs.CONCUR.2025.21'
apa: 'Henzinger, T. A., Kebis, P., Mazzocchi, N. A., & Sarac, N. E. (2025).
Quantitative language automata. In 36th International Conference on Concurrency
Theory (Vol. 348). Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2025.21'
chicago: Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E
Sarac. “Quantitative Language Automata.” In 36th International Conference on
Concurrency Theory, Vol. 348. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025. https://doi.org/10.4230/LIPIcs.CONCUR.2025.21.
ieee: T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Quantitative
language automata,” in 36th International Conference on Concurrency Theory,
Aarhus, Denmark, 2025, vol. 348.
ista: 'Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2025. Quantitative language
automata. 36th International Conference on Concurrency Theory. CONCUR: Conference
on Concurrency Theory, LIPIcs, vol. 348, 21.'
mla: Henzinger, Thomas A., et al. “Quantitative Language Automata.” 36th International
Conference on Concurrency Theory, vol. 348, 21, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025, doi:10.4230/LIPIcs.CONCUR.2025.21.
short: T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 36th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025.
conference:
end_date: 2025-08-29
location: Aarhus, Denmark
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2025-08-26
corr_author: '1'
date_created: 2025-08-31T22:01:32Z
date_published: 2025-08-18T00:00:00Z
date_updated: 2025-12-01T12:36:52Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2025.21
ec_funded: 1
external_id:
arxiv:
- '2506.0515'
isi:
- '001570540800021'
file:
- access_level: open_access
checksum: 9d4054058757a73477e6015b10ed6996
content_type: application/pdf
creator: dernst
date_created: 2025-09-03T10:01:53Z
date_updated: 2025-09-03T10:01:53Z
file_id: '20282'
file_name: 2025_CONCUR_HenzingerT.pdf
file_size: 1257397
relation: main_file
success: 1
file_date_updated: 2025-09-03T10:01:53Z
has_accepted_license: '1'
intvolume: ' 348'
isi: 1
language:
- iso: eng
month: '08'
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: 36th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783959773898'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative language automata
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: 348
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: gold
_id: '20290'
abstract:
- lang: eng
text: 'We consider equilibria in multiplayer stochastic graph games with terminal-node
rewards. In such games, Nash equilibria are defined assuming that each player
seeks to maximise their expected payoff, ignoring their aversion or tolerance
to risk. We therefore study risk-sensitive equilibria (RSEs), where the expected
payoff is replaced by a risk measure. A classical risk measure in the literature
is the entropic risk measure, where each player has a real valued parameter capturing
their risk-averseness. We introduce the extreme risk measure, which corresponds
to extreme cases of entropic risk measure, where players are either extreme optimists
or extreme pessimists. Under extreme risk measure, every player is an extremist:
an extreme optimist perceives their reward as the maximum payoff that can be achieved
with positive probability, while an extreme pessimist expects the minimum payoff
achievable with positive probability. We argue that the extreme risk measure,
especially in multi-player graph based settings, is particularly relevant as they
can model several real life instances such as interactions between secure systems
and potential security threats, or distributed controls for safety critical systems.
We prove that RSEs defined with the extreme risk measure are guaranteed to exist
when all rewards are non-negative. Furthermore, we prove that the problem of deciding
whether a given game contains an RSE that generates risk measures within specified
intervals is decidable and NP-complete for our extreme risk measure, and even
PTIME-complete when all players are extreme optimists, while that same problem
is undecidable using the entropic risk measure or even the classical expected
payoff. This establishes, to our knowledge, the first decidable fragment for equilibria
in simple stochastic games without restrictions on strategy types or number of
players.'
acknowledgement: "This work is a part of project VAMOS that has received funding from
the European\r\nResearch Council (ERC), grant agreement No 101020093. We thank anonymous
reviewers for pointing us to the Hurwicz criterion and to the work of Gallego-Hernández
and Mansutti [13]. We thank Marie van den Bogaard for her valuable feedback on the
first author’s PhD dissertation, which helped improve the quality of this work. "
alternative_title:
- LIPIcs
article_number: '30'
article_processing_charge: Yes
arxiv: 1
author:
- first_name: Léonard
full_name: Brice, Léonard
last_name: Brice
- 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: K. S.
full_name: Thejaswini, K. S.
id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
last_name: Thejaswini
citation:
ama: 'Brice L, Henzinger TA, Thejaswini KS. Finding equilibria: Simpler for pessimists,
simplest for optimists. In: 50th International Symposium on Mathematical Foundations
of Computer Science. Vol 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2025. doi:10.4230/LIPIcs.MFCS.2025.30'
apa: 'Brice, L., Henzinger, T. A., & Thejaswini, K. S. (2025). Finding equilibria:
Simpler for pessimists, simplest for optimists. In 50th International Symposium
on Mathematical Foundations of Computer Science (Vol. 345). Warsaw, Poland:
Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2025.30'
chicago: 'Brice, Léonard, Thomas A Henzinger, and K. S. Thejaswini. “Finding Equilibria:
Simpler for Pessimists, Simplest for Optimists.” In 50th International Symposium
on Mathematical Foundations of Computer Science, Vol. 345. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/LIPIcs.MFCS.2025.30.'
ieee: 'L. Brice, T. A. Henzinger, and K. S. Thejaswini, “Finding equilibria: Simpler
for pessimists, simplest for optimists,” in 50th International Symposium on
Mathematical Foundations of Computer Science, Warsaw, Poland, 2025, vol. 345.'
ista: 'Brice L, Henzinger TA, Thejaswini KS. 2025. Finding equilibria: Simpler for
pessimists, simplest for optimists. 50th International Symposium on Mathematical
Foundations of Computer Science. MFCS: Mathematical Foundations of Computer Science,
LIPIcs, vol. 345, 30.'
mla: 'Brice, Léonard, et al. “Finding Equilibria: Simpler for Pessimists, Simplest
for Optimists.” 50th International Symposium on Mathematical Foundations of
Computer Science, vol. 345, 30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025, doi:10.4230/LIPIcs.MFCS.2025.30.'
short: L. Brice, T.A. Henzinger, K.S. Thejaswini, in:, 50th International Symposium
on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025.
conference:
end_date: 2025-08-29
location: Warsaw, Poland
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2025-08-25
corr_author: '1'
date_created: 2025-09-07T22:01:32Z
date_published: 2025-08-20T00:00:00Z
date_updated: 2025-09-08T07:15:40Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2025.30
ec_funded: 1
external_id:
arxiv:
- '2502.0531'
file:
- access_level: open_access
checksum: 9bc6b8e537662d371d2a27444cbc0b75
content_type: application/pdf
creator: dernst
date_created: 2025-09-08T07:11:12Z
date_updated: 2025-09-08T07:11:12Z
file_id: '20306'
file_name: 2025_MFCS_Brice.pdf
file_size: 1149694
relation: main_file
success: 1
file_date_updated: 2025-09-08T07:11:12Z
has_accepted_license: '1'
intvolume: ' 345'
language:
- iso: eng
month: '08'
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: 50th International Symposium on Mathematical Foundations of Computer
Science
publication_identifier:
isbn:
- '9783959773881'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Finding equilibria: Simpler for pessimists, simplest for optimists'
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: 345
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '20291'
abstract:
- lang: eng
text: "We define and study classes of ω-regular automata for which the nondeterminism
can be resolved by a policy that uses a combination of memory and randomness on
any input word, based solely on the prefix read so far. We examine two settings
for providing the input word to an automaton. In the first setting, called adversarial
resolvability, the input word is constructed letter-by-letter by an adversary,
dependent on the resolver’s previous decisions. In the second setting, called
stochastic resolvability, the adversary pre-commits to an infinite word and reveals
it letter-by-letter. In each setting, we require the existence of an almost-sure
resolver, i.e., a policy that ensures that as long as the adversary provides a
word in the language of the underlying nondeterministic automaton, the run constructed
by the policy is accepting with probability 1.\r\nThe class of automata that are
adversarially resolvable is the well-studied class of history-deterministic automata.
The case of stochastically resolvable automata, on the other hand, defines a novel
class. Restricting the class of resolvers in both settings to stochastic policies
without memory introduces two additional new classes of automata. We show that
the new automata classes offer interesting trade-offs between succinctness, expressivity,
and computational complexity, providing a fine gradation between deterministic
automata and nondeterministic automata."
acknowledgement: This work is a part of project VAMOS that has received funding from
the European Research Council (ERC), grant agreement No 101020093.
alternative_title:
- LIPIcs
article_number: '57'
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: Aditya
full_name: Prakash, Aditya
last_name: Prakash
- first_name: K. S.
full_name: Thejaswini, K. S.
id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
last_name: Thejaswini
citation:
ama: 'Henzinger TA, Prakash A, Thejaswini KS. Resolving nondeterminism with randomness.
In: 50th International Symposium on Mathematical Foundations of Computer Science.
Vol 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:10.4230/LIPIcs.MFCS.2025.57'
apa: 'Henzinger, T. A., Prakash, A., & Thejaswini, K. S. (2025). Resolving nondeterminism
with randomness. In 50th International Symposium on Mathematical Foundations
of Computer Science (Vol. 345). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2025.57'
chicago: Henzinger, Thomas A, Aditya Prakash, and K. S. Thejaswini. “Resolving Nondeterminism
with Randomness.” In 50th International Symposium on Mathematical Foundations
of Computer Science, Vol. 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025. https://doi.org/10.4230/LIPIcs.MFCS.2025.57.
ieee: T. A. Henzinger, A. Prakash, and K. S. Thejaswini, “Resolving nondeterminism
with randomness,” in 50th International Symposium on Mathematical Foundations
of Computer Science, Warsaw, Poland, 2025, vol. 345.
ista: 'Henzinger TA, Prakash A, Thejaswini KS. 2025. Resolving nondeterminism with
randomness. 50th International Symposium on Mathematical Foundations of Computer
Science. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 345,
57.'
mla: Henzinger, Thomas A., et al. “Resolving Nondeterminism with Randomness.” 50th
International Symposium on Mathematical Foundations of Computer Science, vol.
345, 57, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:10.4230/LIPIcs.MFCS.2025.57.
short: T.A. Henzinger, A. Prakash, K.S. Thejaswini, in:, 50th International Symposium
on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2025.
conference:
end_date: 2025-08-29
location: Warsaw, Poland
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2025-08-25
corr_author: '1'
date_created: 2025-09-07T22:01:32Z
date_published: 2025-08-20T00:00:00Z
date_updated: 2025-09-08T07:06:11Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2025.57
ec_funded: 1
external_id:
arxiv:
- '2502.12872'
file:
- access_level: open_access
checksum: 6068b772aba6cb0d01f3e5a90abed973
content_type: application/pdf
creator: dernst
date_created: 2025-09-08T06:56:56Z
date_updated: 2025-09-08T06:56:56Z
file_id: '20305'
file_name: 2025_MFCS_HenzingerT.pdf
file_size: 1009644
relation: main_file
success: 1
file_date_updated: 2025-09-08T06:56:56Z
has_accepted_license: '1'
intvolume: ' 345'
language:
- iso: eng
month: '08'
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: 50th International Symposium on Mathematical Foundations of Computer
Science
publication_identifier:
isbn:
- '9783959773881'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Resolving nondeterminism with randomness
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: 345
year: '2025'
...
---
OA_place: publisher
_id: '20292'
abstract:
- lang: eng
text: In automated decision-making, it is desirable that outputs of decision-makers
be robust to slight perturbations in their inputs, a property that may be called
input-output robustness. Input-output robustness appears in various different
forms in the literature, such as robustness of AI models to adversarial or semantic
perturbations and individual fairness of AI models that make decisions about humans.
We propose runtime monitoring of input-output robustness of deployed, black-box
AI models, where the goal is to design monitors that would observe one long execution
sequence of the model, and would raise an alarm whenever it is detected that two
similar inputs from the past led to dissimilar outputs. This way, monitoring will
complement existing offline ''robustification'' approaches to increase the trustworthiness
of AI decision-makers. We show that the monitoring problem can be cast as the
fixed-radius nearest neighbor (FRNN) search problem, which, despite being well-studied,
lacks suitable online solutions. We present our tool Clemont, which offers a number
of lightweight monitors, some of which use upgraded online variants of existing
FRNN algorithms, and one uses a novel algorithm based on binary decision diagrams--a
data-structure commonly used in software and hardware verification. We have also
developed an efficient parallelization technique that can substantially cut down
the computation time of monitors for which the distance between input-output pairs
is measured using the L∞norm. Using standard benchmarks from the literature of
adversarial and semantic robustness and individual fairness, we perform a comparative
study of different monitors in Clemont, and demonstrate their effectiveness in
correctly detecting robustness violations at runtime.
acknowledgement: This work was supported in part by the ERC project ERC-2020-AdG 101020093
and the SBI Foundation Hub for Data Science &Analytics, IIT Bombay.
article_processing_charge: No
arxiv: 1
author:
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- 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: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: David
full_name: Pape, David
last_name: Pape
citation:
ama: 'Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. Monitoring robustness
and individual fairness. In: Proceedings of the 31st ACM SIGKDD Conference
on Knowledge Discovery and Data Mining. Vol 2. Association for Computing Machinery;
2025:790-801. doi:10.1145/3711896.3737054'
apa: 'Gupta, A., Henzinger, T. A., Kueffner, K., Mallik, K., & Pape, D. (2025).
Monitoring robustness and individual fairness. In Proceedings of the 31st ACM
SIGKDD Conference on Knowledge Discovery and Data Mining (Vol. 2, pp. 790–801).
Toronto, Canada: Association for Computing Machinery. https://doi.org/10.1145/3711896.3737054'
chicago: Gupta, Ashutosh, Thomas A Henzinger, Konstantin Kueffner, Kaushik Mallik,
and David Pape. “Monitoring Robustness and Individual Fairness.” In Proceedings
of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining,
2:790–801. Association for Computing Machinery, 2025. https://doi.org/10.1145/3711896.3737054.
ieee: A. Gupta, T. A. Henzinger, K. Kueffner, K. Mallik, and D. Pape, “Monitoring
robustness and individual fairness,” in Proceedings of the 31st ACM SIGKDD
Conference on Knowledge Discovery and Data Mining, Toronto, Canada, 2025,
vol. 2, pp. 790–801.
ista: 'Gupta A, Henzinger TA, Kueffner K, Mallik K, Pape D. 2025. Monitoring robustness
and individual fairness. Proceedings of the 31st ACM SIGKDD Conference on Knowledge
Discovery and Data Mining. KDD: Conference on Knowledge Discovery and Data Mining
vol. 2, 790–801.'
mla: Gupta, Ashutosh, et al. “Monitoring Robustness and Individual Fairness.” Proceedings
of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining,
vol. 2, Association for Computing Machinery, 2025, pp. 790–801, doi:10.1145/3711896.3737054.
short: A. Gupta, T.A. Henzinger, K. Kueffner, K. Mallik, D. Pape, in:, Proceedings
of the 31st ACM SIGKDD Conference on Knowledge Discovery and Data Mining, Association
for Computing Machinery, 2025, pp. 790–801.
conference:
end_date: 2025-08-07
location: Toronto, Canada
name: 'KDD: Conference on Knowledge Discovery and Data Mining'
start_date: 2025-08-03
corr_author: '1'
date_created: 2025-09-07T22:01:33Z
date_published: 2025-08-03T00:00:00Z
date_updated: 2025-09-08T08:54:24Z
day: '03'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3711896.3737054
ec_funded: 1
external_id:
arxiv:
- '2506.00496'
file:
- access_level: open_access
checksum: 81e18cdf9ca5f6dfa79425b326ea9725
content_type: application/pdf
creator: dernst
date_created: 2025-09-08T08:46:31Z
date_updated: 2025-09-08T08:46:31Z
file_id: '20310'
file_name: 2025_KDD_Gupta.pdf
file_size: 7745940
relation: main_file
success: 1
file_date_updated: 2025-09-08T08:46:31Z
has_accepted_license: '1'
intvolume: ' 2'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 790-801
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 31st ACM SIGKDD Conference on Knowledge Discovery
and Data Mining
publication_identifier:
isbn:
- '9798400714542'
issn:
- 2154-817X
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/ariez-xyz/clemont
scopus_import: '1'
status: public
title: Monitoring robustness and individual fairness
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: 2
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'
...
---
OA_place: repository
OA_type: green
_id: '20723'
abstract:
- lang: eng
text: Information-flow interfaces is a formalism recently proposed for specifying,
composing, and refining system-wide security requirements. In this work, we show
how the widely used concept of security lattices provides a natural semantic interpretation
for information-flow interfaces.
acknowledgement: This project was funded in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe F8502 and by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- 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: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-Flow
Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber
Physical Systems. Vol 15471. Cham: Springer Nature; 2025:251-263. doi:10.1007/978-3-031-97537-0_15'
apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A.
(2025). Information-Flow Interfaces and Security Lattices. In Engineering Safe
and Trustworthy Cyber Physical Systems (Vol. 15471, pp. 251–263). Cham: Springer
Nature. https://doi.org/10.1007/978-3-031-97537-0_15'
chicago: 'Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da
Costa. “Information-Flow Interfaces and Security Lattices.” In Engineering
Safe and Trustworthy Cyber Physical Systems, 15471:251–63. Cham: Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-97537-0_15.'
ieee: 'E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-Flow
Interfaces and Security Lattices,” in Engineering Safe and Trustworthy Cyber
Physical Systems, vol. 15471, Cham: Springer Nature, 2025, pp. 251–263.'
ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.Information-Flow
Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber Physical
Systems. LNCS, vol. 15471, 251–263.'
mla: Bartocci, Ezio, et al. “Information-Flow Interfaces and Security Lattices.”
Engineering Safe and Trustworthy Cyber Physical Systems, vol. 15471, Springer
Nature, 2025, pp. 251–63, doi:10.1007/978-3-031-97537-0_15.
short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, Engineering
Safe and Trustworthy Cyber Physical Systems, Springer Nature, Cham, 2025, pp.
251–263.
corr_author: '1'
date_created: 2025-12-01T15:44:58Z
date_published: 2025-10-02T00:00:00Z
date_updated: 2025-12-09T07:57:55Z
day: '02'
department:
- _id: ToHe
doi: 10.1007/978-3-031-97537-0_15
ec_funded: 1
external_id:
arxiv:
- '2406.14374'
intvolume: ' 15471'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2406.14374
month: '10'
oa: 1
oa_version: Preprint
page: 251-263
place: Cham
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Engineering Safe and Trustworthy Cyber Physical Systems
publication_identifier:
eisbn:
- '9783031975370'
eissn:
- 1611-3349
isbn:
- '9783031975363'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Information-Flow Interfaces and Security Lattices
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15471
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19665'
abstract:
- lang: eng
text: As AI-based decision-makers increasingly influence human lives, it is a growing
concern that their decisions may be unfair or biased with respect to people's
protected attributes, such as gender and race. Most existing bias prevention measures
provide probabilistic fairness guarantees in the long run, and it is possible
that the decisions are biased on any decision sequence of fixed length. We introduce
*fairness shielding*, where a symbolic decision-maker---the fairness shield---continuously
monitors the sequence of decisions of another deployed black-box decision-maker,
and makes interventions so that a given fairness criterion is met while the total
intervention costs are minimized. We present four different algorithms for computing
fairness shields, among which one guarantees fairness over fixed horizons, and
three guarantee fairness periodically after fixed intervals. Given a distribution
over future decisions and their intervention costs, our algorithms solve different
instances of bounded-horizon optimal control problems with different levels of
computational costs and optimality guarantees. Our empirical evaluation demonstrates
the effectiveness of these shields in ensuring fairness while maintaining cost
efficiency across various scenarios.
acknowledgement: 'This work is partly supported by the European Research Council under
Grant No.: ERC-2020-AdG 101020093. It is also partially supported by the State Government
of Styria, Austria – Department Zukunftsfonds Steiermark.'
article_processing_charge: No
arxiv: 1
author:
- first_name: Filip
full_name: Cano Cordoba, Filip
id: 708cad98-e86a-11ef-8098-bdae2d7c6af1
last_name: Cano Cordoba
orcid: 0000-0002-0783-904X
- 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: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
citation:
ama: 'Cano Cordoba F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. Fairness
shields: Safeguarding against biased decision makers. In: Proceedings of the
39th AAAI Conference on Artificial Intelligence. Vol 39. Association for the
Advancement of Artificial Intelligence; 2025:15659-15668. doi:10.1609/aaai.v39i15.33719'
apa: 'Cano Cordoba, F., Henzinger, T. A., Könighofer, B., Kueffner, K., & Mallik,
K. (2025). Fairness shields: Safeguarding against biased decision makers. In Proceedings
of the 39th AAAI Conference on Artificial Intelligence (Vol. 39, pp. 15659–15668).
Philadelphia, PA, United States: Association for the Advancement of Artificial
Intelligence. https://doi.org/10.1609/aaai.v39i15.33719'
chicago: 'Cano Cordoba, Filip, Thomas A Henzinger, Bettina Könighofer, Konstantin
Kueffner, and Kaushik Mallik. “Fairness Shields: Safeguarding against Biased Decision
Makers.” In Proceedings of the 39th AAAI Conference on Artificial Intelligence,
39:15659–68. Association for the Advancement of Artificial Intelligence, 2025.
https://doi.org/10.1609/aaai.v39i15.33719.'
ieee: 'F. Cano Cordoba, T. A. Henzinger, B. Könighofer, K. Kueffner, and K. Mallik,
“Fairness shields: Safeguarding against biased decision makers,” in Proceedings
of the 39th AAAI Conference on Artificial Intelligence, Philadelphia, PA,
United States, 2025, vol. 39, no. 15, pp. 15659–15668.'
ista: 'Cano Cordoba F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. 2025. Fairness
shields: Safeguarding against biased decision makers. Proceedings of the 39th
AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence
vol. 39, 15659–15668.'
mla: 'Cano Cordoba, Filip, et al. “Fairness Shields: Safeguarding against Biased
Decision Makers.” Proceedings of the 39th AAAI Conference on Artificial Intelligence,
vol. 39, no. 15, Association for the Advancement of Artificial Intelligence, 2025,
pp. 15659–68, doi:10.1609/aaai.v39i15.33719.'
short: F. Cano Cordoba, T.A. Henzinger, B. Könighofer, K. Kueffner, K. Mallik, in:,
Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association
for the Advancement of Artificial Intelligence, 2025, pp. 15659–15668.
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:39Z
date_published: 2025-04-11T00:00:00Z
date_updated: 2026-02-16T12:24:30Z
day: '11'
department:
- _id: ToHe
doi: 10.1609/aaai.v39i15.33719
ec_funded: 1
external_id:
arxiv:
- '2412.11994'
intvolume: ' 39'
issue: '15'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2412.11994
month: '04'
oa: 1
oa_version: Preprint
page: 15659-15668
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: 'Fairness shields: Safeguarding against biased decision makers'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 39
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: '19739'
abstract:
- lang: eng
text: "Cooperative verification is gaining momentum in recent years. The usual setup
in cooperative verification is that a verifier A is run with some pre-defined
resources, and if it is not able to verify the program, the verification task
is passed to a verifier B together with information learned about the program
by verifier A, then the chain can continue to a verifier C, and so on. This scheme
is static: tools run one after another in a fixed pre-defined order and fixed
parameters and resource limits (the scheme may differ for properties to be analyzed,
though).\r\n\r\nBubaak is a program analysis tool that allows to run multiple
program verifiers in a dynamically changing combination of parallel and sequential
portfolios. Bubaak starts the verification process by invoking an initial set
of tasks; every task, when it is done (e.g., because of hitting a time limit or
finishing its job), rewrites itself into one or more successor tasks. New tasks
can be also spawned upon events generated by other tasks. This all happens dynamically
based on the information gathered by finished and running tasks. During their
execution, tasks that run in parallel can exchange (partial) verification artifacts,
either directly or with Bubaak as an intermediary."
acknowledgement: This work was in part supported by the ERC-2020-AdG 10102009 grant,
and in part by the German Research Foundation (DFG) - WE2290/13-2 (Coop2).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Cedric
full_name: Richter, Cedric
last_name: Richter
citation:
ama: 'Chalupa M, Richter C. BUBAAK: Dynamic cooperative verification. In: 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. Vol 15698. Springer Nature; 2025:212-216. doi:10.1007/978-3-031-90660-2_14'
apa: 'Chalupa, M., & Richter, C. (2025). BUBAAK: Dynamic cooperative verification.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15698, pp. 212–216). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90660-2_14'
chicago: 'Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.”
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 15698:212–16. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-90660-2_14.'
ieee: 'M. Chalupa and C. Richter, “BUBAAK: Dynamic cooperative verification,” in
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Hamilton, ON, Canada, 2025, vol. 15698, pp. 212–216.'
ista: 'Chalupa M, Richter C. 2025. BUBAAK: Dynamic cooperative verification. 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
LNCS, vol. 15698, 212–216.'
mla: 'Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.”
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 15698, Springer Nature, 2025, pp. 212–16, doi:10.1007/978-3-031-90660-2_14.'
short: M. Chalupa, C. Richter, in:, 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 212–216.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:04Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T07:21:41Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-90660-2_14
ec_funded: 1
file:
- access_level: open_access
checksum: 3f604f25dbe37383acb7f8308aad3ca6
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T07:10:35Z
date_updated: 2025-06-02T07:10:35Z
file_id: '19766'
file_name: 2025_TACAS_Chalupa.pdf
file_size: 259050
relation: main_file
success: 1
file_date_updated: 2025-06-02T07:10:35Z
has_accepted_license: '1'
intvolume: ' 15698'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 212-216
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906596'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'BUBAAK: Dynamic cooperative verification'
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: 15698
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20866'
abstract:
- lang: eng
text: In this work, we present hypernode automata as a specification formalism for
hyperproperties of systems whose executions may be misaligned among themselves,
such as concurrent systems. These automata consist of nodes labeled with hypernode
logic formulas and transitions marked with synchronizing actions. Hypernode logic
formulas establish relations between sequences of variable values among different
system executions. This logic enables both synchronous and asynchronous analysis
of traces. In its asynchronous view on execution traces, hypernode formulas establish
relations on the order of value changes for each variable without correlating
their timing. In both views, the analysis of different execution traces is synchronized
through the transitions of hypernode automata. By combining logic’s declarative
nature with automata’s procedural power, hypernode automata seamlessly integrate
asynchronicity requirements at the node level with synchronicity between node
transitions. We show that the model-checking problem for hypernode automata is
decidable for specifications where each node specifies either a synchronous or
an asynchronous requirement for the system’s executions, but not both.
acknowledgement: This work was supported in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe 10.55776/F85, by the FWF projects ZK-35 and W1255-N23, and by
the ERC Advanced Grant VAMOS 101020093. Open access funding provided by Institute
of Science and Technology (IST Austria).
article_number: '43'
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- 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: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode
automata. Acta Informatica. 2025;62(4). doi:10.1007/s00236-025-00509-8
apa: Bartocci, E., Chalupa, M., Henzinger, T. A., Nickovic, D., & Oliveira da
Costa, A. (2025). Hypernode automata. Acta Informatica. Springer Nature.
https://doi.org/10.1007/s00236-025-00509-8
chicago: Bartocci, Ezio, Marek Chalupa, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira da Costa. “Hypernode Automata.” Acta Informatica. Springer
Nature, 2025. https://doi.org/10.1007/s00236-025-00509-8.
ieee: E. Bartocci, M. Chalupa, T. A. Henzinger, D. Nickovic, and A. Oliveira da
Costa, “Hypernode automata,” Acta Informatica, vol. 62, no. 4. Springer
Nature, 2025.
ista: Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.
Hypernode automata. Acta Informatica. 62(4), 43.
mla: Bartocci, Ezio, et al. “Hypernode Automata.” Acta Informatica, vol.
62, no. 4, 43, Springer Nature, 2025, doi:10.1007/s00236-025-00509-8.
short: E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa,
Acta Informatica 62 (2025).
corr_author: '1'
date_created: 2025-12-29T12:07:12Z
date_published: 2025-12-09T00:00:00Z
date_updated: 2026-01-05T12:27:41Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00236-025-00509-8
ec_funded: 1
external_id:
arxiv:
- '2305.02836'
file:
- access_level: open_access
checksum: 06ed45a1218ad8464818803ae2968aaf
content_type: application/pdf
creator: dernst
date_created: 2026-01-05T12:26:43Z
date_updated: 2026-01-05T12:26:43Z
file_id: '20944'
file_name: 2025_ActaInformatica_Bartocci.pdf
file_size: 7117003
relation: main_file
success: 1
file_date_updated: 2026-01-05T12:26:43Z
has_accepted_license: '1'
intvolume: ' 62'
issue: '4'
language:
- iso: eng
month: '12'
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
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14405'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Hypernode automata
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 62
year: '2025'
...