---
OA_place: publisher
OA_type: hybrid
_id: '22006'
abstract:
- lang: eng
text: Runtime monitoring checks, during execution, whether a partial signal produced
by a hybrid system satisfies its specification. Signal First-Order Logic (SFO)
offers expressive real-time specifications over such signals, but currently comes
only with Boolean semantics and has no tool support. We provide the first robustness-based
quantitative semantics for SFO, enabling the expression and evaluation of rich
real-time properties beyond the scope of existing formalisms such as Signal Temporal
Logic. To enable online monitoring, we identify a past-time fragment of SFO and
give a pastification procedure that transforms bounded-response SFO formulas into
equisatisfiable formulas in this fragment. We then develop an efficient runtime
monitoring algorithm for this past-time fragment and evaluate its performance
on a set of benchmarks, demonstrating the practicality and effectiveness of our
approach. To the best of our knowledge, this is the first publicly available prototype
for online quantitative monitoring of full SFO.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported by the European Research Council (ERC) Grants VAMOS (No. 101020093)
and HYPER (No. 101055412), and by the Advanced Research and Invention Agency under
the Safeguarded AI programme (MSAI-PR01-P047).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
citation:
ama: 'Chalupa M, Henzinger TA, Sarac NE, Yu E. Quantitative monitoring of Signal
First-Order logic. In: 27th International Symposium on Formal Methods.
Vol 16557. Springer Nature; 2026:214-233. doi:10.1007/978-3-032-26220-2_11'
apa: 'Chalupa, M., Henzinger, T. A., Sarac, N. E., & Yu, E. (2026). Quantitative
monitoring of Signal First-Order logic. In 27th International Symposium on
Formal Methods (Vol. 16557, pp. 214–233). Tokyo, Japan: Springer Nature. https://doi.org/10.1007/978-3-032-26220-2_11'
chicago: Chalupa, Marek, Thomas A Henzinger, Naci E Sarac, and Emily Yu. “Quantitative
Monitoring of Signal First-Order Logic.” In 27th International Symposium on
Formal Methods, 16557:214–33. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-26220-2_11.
ieee: M. Chalupa, T. A. Henzinger, N. E. Sarac, and E. Yu, “Quantitative monitoring
of Signal First-Order logic,” in 27th International Symposium on Formal Methods,
Tokyo, Japan, 2026, vol. 16557, pp. 214–233.
ista: 'Chalupa M, Henzinger TA, Sarac NE, Yu E. 2026. Quantitative monitoring of Signal
First-Order logic. 27th International Symposium on Formal Methods. FM: Formal
Methods, LNCS, vol. 16557, 214–233.'
mla: Chalupa, Marek, et al. “Quantitative Monitoring of Signal First-Order Logic.”
27th International Symposium on Formal Methods, vol. 16557, Springer Nature,
2026, pp. 214–33, doi:10.1007/978-3-032-26220-2_11.
short: M. Chalupa, T.A. Henzinger, N.E. Sarac, E. Yu, in:, 27th International Symposium
on Formal Methods, Springer Nature, 2026, pp. 214–233.
conference:
end_date: 2026-05-22
location: Tokyo, Japan
name: 'FM: Formal Methods'
start_date: 2026-05-18
das_tickbox: '0'
date_created: 2026-06-14T22:01:44Z
date_published: 2026-05-18T00:00:00Z
date_updated: 2026-06-22T08:21:09Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-032-26220-2_11
ec_funded: 1
external_id:
arxiv:
- '2603.00728'
file:
- access_level: open_access
checksum: 7055199ecb985e9e2e272f4988827067
content_type: application/pdf
creator: dernst
date_created: 2026-06-22T08:18:41Z
date_updated: 2026-06-22T08:18:41Z
file_id: '22113'
file_name: 2026_LNCS_Chalupa.pdf
file_size: 849237
relation: main_file
success: 1
file_date_updated: 2026-06-22T08:18:41Z
has_accepted_license: '1'
intvolume: ' 16557'
keyword:
- Signal first-order logic
- Robustness-based quantitative semantics
- Online runtime monitoring
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 214-233
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 27th International Symposium on Formal Methods
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032262196'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative monitoring of Signal First-Order logic
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16557
year: '2026'
...
---
OA_place: 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
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: repository
OA_type: green
_id: '22103'
abstract:
- lang: eng
text: "Modern AI systems increasingly rely on opaque, highly complex models whose
inner workings remain inaccessible even to experts. This opacity creates challenges
for trust, accountability, and compliance with\r\nemerging regulatory expectations
such as the “right to an explanation”. While traditional explainability methods—feature
attributions, counterfactuals, surrogate models—and interpretable model classes
provide valuable insights for engineers, they often fall short of delivering the
contextual, conversational explanations that\r\nreal users expect. Large Language
Models (LLMs) offer a promising new avenue for explanation due to their\r\nability
to engage interactively, adapt to user needs, and translate technical outputs
into more accessible reasoning. However, their tendencies toward hallucination,
conflict avoidance, and oversimplification introduce\r\nserious risks when used
as explanatory agents. This paper analyzes these opportunities and limitations,
examines verification strategies for ensuring explanation fidelity, and situates
LLM-generated explanations within\r\nbroader concerns about public trust. The
paper concludes by outlining best practices and future research directions for
building robust, verifiable, and human-aligned explanation systems."
acknowledgement: "This work has been supported by the European Research Council under
Grant No.: ERC-2020-AdG\r\n101020093. LLM–based tools have been used as\r\nwriting
assistance to help improve presentation.\r\n"
article_processing_charge: No
author:
- first_name: Filip
full_name: Cano Cordoba, Filip
id: 708cad98-e86a-11ef-8098-bdae2d7c6af1
last_name: Cano Cordoba
orcid: 0000-0002-0783-904X
citation:
ama: 'Cano Cordoba F. Explaining decisions one conversation at a time: Opportunities
and risks of LLMs as explainability assistants. In: Proceedings of the 18th
International Conference on Agents and Artificial Intelligence. Vol 5. Science
and Technology Publications; 2026:4689-4696. doi:10.5220/0014483200004052'
apa: 'Cano Cordoba, F. (2026). Explaining decisions one conversation at a time:
Opportunities and risks of LLMs as explainability assistants. In Proceedings
of the 18th International Conference on Agents and Artificial Intelligence
(Vol. 5, pp. 4689–4696). Marbella, Spain: Science and Technology Publications.
https://doi.org/10.5220/0014483200004052'
chicago: 'Cano Cordoba, Filip. “Explaining Decisions One Conversation at a Time:
Opportunities and Risks of LLMs as Explainability Assistants.” In Proceedings
of the 18th International Conference on Agents and Artificial Intelligence,
5:4689–96. Science and Technology Publications, 2026. https://doi.org/10.5220/0014483200004052.'
ieee: 'F. Cano Cordoba, “Explaining decisions one conversation at a time: Opportunities
and risks of LLMs as explainability assistants,” in Proceedings of the 18th
International Conference on Agents and Artificial Intelligence, Marbella,
Spain, 2026, vol. 5, pp. 4689–4696.'
ista: 'Cano Cordoba F. 2026. Explaining decisions one conversation at a time: Opportunities
and risks of LLMs as explainability assistants. Proceedings of the 18th International
Conference on Agents and Artificial Intelligence. ICAART: International Conference
on Agents and Artificial Intelligence vol. 5, 4689–4696.'
mla: 'Cano Cordoba, Filip. “Explaining Decisions One Conversation at a Time: Opportunities
and Risks of LLMs as Explainability Assistants.” Proceedings of the 18th International
Conference on Agents and Artificial Intelligence, vol. 5, Science and Technology
Publications, 2026, pp. 4689–96, doi:10.5220/0014483200004052.'
short: F. Cano Cordoba, in:, Proceedings of the 18th International Conference on
Agents and Artificial Intelligence, Science and Technology Publications, 2026,
pp. 4689–4696.
conference:
end_date: 2026-03-08
location: Marbella, Spain
name: 'ICAART: International Conference on Agents and Artificial Intelligence'
start_date: 2026-03-05
corr_author: '1'
das_tickbox: '0'
date_created: 2026-06-21T22:03:00Z
date_published: 2026-04-01T00:00:00Z
date_updated: 2026-06-24T08:37:00Z
day: '01'
department:
- _id: ToHe
doi: 10.5220/0014483200004052
ec_funded: 1
intvolume: ' 5'
keyword:
- Explainable AI
- Large Language Models
- Trust in AI
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://filipcano.org/files/icaart26llm.pdf
month: '04'
oa: 1
oa_version: Accepted Version
page: 4689-4696
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 18th International Conference on Agents and Artificial
Intelligence
publication_identifier:
eissn:
- 2184-433X
isbn:
- '9789897587962'
issn:
- 2184-3589
publication_status: published
publisher: Science and Technology Publications
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Explaining decisions one conversation at a time: Opportunities and risks of
LLMs as explainability assistants'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5
year: '2026'
...
---
OA_type: closed access
_id: '22300'
abstract:
- lang: eng
text: As seen in previous chapters, a graph game proceeds by placing a token on
one of the vertices and allowing the players to move it throughout the graph to
produce an infinite trace, which determines the winner or payoff of the game.
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- 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: 'Avni G, Henzinger TA. Bidding Games. In: Fijalkow Nathanaël, ed. Games
on Graphs. From Logic and Automata to Algorithms. Cambridge University Press;
2026:529-569. doi:10.1017/9781009500678.022'
apa: Avni, G., & Henzinger, T. A. (2026). Bidding Games. In Nathanaël Fijalkow
(Ed.), Games on Graphs. From Logic and Automata to Algorithms (pp. 529–569).
Cambridge University Press. https://doi.org/10.1017/9781009500678.022
chicago: Avni, Guy, and Thomas A Henzinger. “Bidding Games.” In Games on Graphs.
From Logic and Automata to Algorithms, edited by Nathanaël Fijalkow, 529–69.
Cambridge University Press, 2026. https://doi.org/10.1017/9781009500678.022.
ieee: G. Avni and T. A. Henzinger, “Bidding Games,” in Games on Graphs. From
Logic and Automata to Algorithms, Nathanaël Fijalkow, Ed. Cambridge University
Press, 2026, pp. 529–569.
ista: 'Avni G, Henzinger TA. 2026.Bidding Games. In: Games on Graphs. From Logic
and Automata to Algorithms. , 529–569.'
mla: Avni, Guy, and Thomas A. Henzinger. “Bidding Games.” Games on Graphs. From
Logic and Automata to Algorithms, edited by Nathanaël Fijalkow, Cambridge
University Press, 2026, pp. 529–69, doi:10.1017/9781009500678.022.
short: G. Avni, T.A. Henzinger, in:, Nathanaël Fijalkow (Ed.), Games on Graphs.
From Logic and Automata to Algorithms, Cambridge University Press, 2026, pp. 529–569.
corr_author: '1'
das_tickbox: '1'
date_created: 2026-07-13T10:44:22Z
date_published: 2026-04-26T00:00:00Z
date_updated: 2026-07-13T13:32:47Z
day: '26'
department:
- _id: ToHe
doi: 10.1017/9781009500678.022
editor:
- first_name: ' Nathanaël'
full_name: Fijalkow, Nathanaël
last_name: Fijalkow
language:
- iso: eng
month: '04'
oa_version: None
page: 529-569
publication: Games on Graphs. From Logic and Automata to Algorithms
publication_identifier:
eisbn:
- '9781009500678'
isbn:
- '9781009500685'
publication_status: published
publisher: Cambridge University Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Bidding Games
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2026'
...
---
OA_place: repository
OA_type: green
_id: '22294'
abstract:
- lang: eng
text: 'Modern computer systems store vast amounts of personal data, enabling advances
in AI and ML but risking user privacy and trust. For privacy reasons, it is sometimes
desired for an ML model to forget part of the data it was trained on. In this
paper, we introduce a novel unlearning approach based on Forgetting Neural Networks
(FNNs), a neuroscience-inspired architecture that explicitly encodes forgetting
through multiplicative decay factors. While FNNs had previously been studied as
a theoretical construct, we provide the first concrete implementation and demonstrate
their effectiveness for targeted unlearning. We propose several variants with
per-neuron forgetting factors, including rank-based assignments guided by activation
levels, and evaluate them on MNIST and Fashion-MNIST benchmarks. Our method systematically
removes information associated with forget sets while preserving performance on
retained data. Membership inference attacks confirm the effectiveness of FNN-based
unlearning in erasing information about the training data from the neural network.
These results establish FNNs as a promising foundation for efficient and interpretable
unlearning. '
article_processing_charge: No
arxiv: 1
author:
- first_name: Amartya
full_name: Hatua, Amartya
last_name: Hatua
- first_name: Trung
full_name: Nguyen, Trung
last_name: Nguyen
- 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: Andrew
full_name: Sung, Andrew
last_name: Sung
citation:
ama: 'Hatua A, Nguyen T, Cano Cordoba F, Sung A. Machine unlearning using forgetting
neural networks. In: Proceedings of the 18th International Conference on Agents
and Artificial Intelligence. Vol 2. SciTePress; 2026:1536-1546. doi:10.5220/0014326500004052'
apa: 'Hatua, A., Nguyen, T., Cano Cordoba, F., & Sung, A. (2026). Machine unlearning
using forgetting neural networks. In Proceedings of the 18th International
Conference on Agents and Artificial Intelligence (Vol. 2, pp. 1536–1546).
Marbella, Spain: SciTePress. https://doi.org/10.5220/0014326500004052'
chicago: Hatua, Amartya, Trung Nguyen, Filip Cano Cordoba, and Andrew Sung. “Machine
Unlearning Using Forgetting Neural Networks.” In Proceedings of the 18th International
Conference on Agents and Artificial Intelligence, 2:1536–46. SciTePress, 2026.
https://doi.org/10.5220/0014326500004052.
ieee: A. Hatua, T. Nguyen, F. Cano Cordoba, and A. Sung, “Machine unlearning using
forgetting neural networks,” in Proceedings of the 18th International Conference
on Agents and Artificial Intelligence, Marbella, Spain, 2026, vol. 2, pp.
1536–1546.
ista: 'Hatua A, Nguyen T, Cano Cordoba F, Sung A. 2026. Machine unlearning using
forgetting neural networks. Proceedings of the 18th International Conference on
Agents and Artificial Intelligence. ICAART: International Conference on Agents
and Artificial Intelligence vol. 2, 1536–1546.'
mla: Hatua, Amartya, et al. “Machine Unlearning Using Forgetting Neural Networks.”
Proceedings of the 18th International Conference on Agents and Artificial Intelligence,
vol. 2, SciTePress, 2026, pp. 1536–46, doi:10.5220/0014326500004052.
short: A. Hatua, T. Nguyen, F. Cano Cordoba, A. Sung, in:, Proceedings of the 18th
International Conference on Agents and Artificial Intelligence, SciTePress, 2026,
pp. 1536–1546.
conference:
end_date: 2026-03-08
location: Marbella, Spain
name: 'ICAART: International Conference on Agents and Artificial Intelligence'
start_date: 2026-03-05
das_tickbox: '1'
date_created: 2026-07-13T09:46:46Z
date_published: 2026-06-30T00:00:00Z
date_updated: 2026-07-16T09:02:53Z
day: '30'
department:
- _id: ToHe
doi: 10.5220/0014326500004052
external_id:
arxiv:
- '2410.22374'
intvolume: ' 2'
keyword:
- Machine Unlearning
- Neuroscience-Inspired Machine Learning
- Membership Inference Attacks
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2410.22374
month: '06'
oa: 1
oa_version: Preprint
page: 1536-1546
publication: Proceedings of the 18th International Conference on Agents and Artificial
Intelligence
publication_identifier:
eissn:
- 2184-433X
isbn:
- '9789897587962'
publication_status: published
publisher: SciTePress
quality_controlled: '1'
scopus_import: '1'
status: public
title: Machine unlearning using forgetting neural networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2026'
...
---
OA_place: publisher
OA_type: gold
_id: '22321'
abstract:
- lang: eng
text: 'Runtime fairness is not a one-time constraint but a dynamic property evaluated
over a sequence of decisions. To ensure fairness at runtime, it is necessary to
account for past decisions, information neglected by conventional, static classifiers.
Traditional fairness shields enforce runtime fairness abruptly, by intervening
deterministically whenever a sequence of decisions violates the target for a running
fairness measure. This motivates our main conceptual contribution: energy shields.
An energy shield is a novel, lightweight, adaptive controller that monitors a
sequence of decisions and intervenes probabilistically to ensure runtime fairness
smoothly, by utilizing physics-inspired energy functions to nudge the sequence
toward fairness: the more unfair the decisions, the stronger the nudging force
becomes. This makes energy shields the first fairness shields to provide both
short-term safety and long-term liveness guarantees. Safety ensures that the running
fairness measure stays within a running target interval with high probability,
and liveness ensures that the limit of the fairness measure lies within the limit
target interval. Intuitively, the short-term specifies the tolerated fairness
values and the long-term specifies the desired fairness values. We also provide
a synthesis procedure for constructing the least intrusive energy shield for a
given target specification, and demonstrate its efficiency experimentally. We
evaluate our energy shields against existing fairness shields through the lens
of short- and long-term fairness.'
acknowledgement: 'This work has been supported by the European Research Council under
Grant No.: ERC-2020-AdG 101020093.'
article_processing_charge: Yes
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: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
citation:
ama: 'Cano Cordoba F, Henzinger TA, Kueffner K. Energy shields for fairness. In:
Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency.
Association for Computing Machinery; 2026:4243-4275. doi:10.1145/3805689.3806807'
apa: 'Cano Cordoba, F., Henzinger, T. A., & Kueffner, K. (2026). Energy shields
for fairness. In Proceedings of the 2026 ACM Conference on Fairness, Accountability,
and Transparency (pp. 4243–4275). Montreal, Canada: Association for Computing
Machinery. https://doi.org/10.1145/3805689.3806807'
chicago: Cano Cordoba, Filip, Thomas A Henzinger, and Konstantin Kueffner. “Energy
Shields for Fairness.” In Proceedings of the 2026 ACM Conference on Fairness,
Accountability, and Transparency, 4243–75. Association for Computing Machinery,
2026. https://doi.org/10.1145/3805689.3806807.
ieee: F. Cano Cordoba, T. A. Henzinger, and K. Kueffner, “Energy shields for fairness,”
in Proceedings of the 2026 ACM Conference on Fairness, Accountability, and
Transparency, Montreal, Canada, 2026, pp. 4243–4275.
ista: 'Cano Cordoba F, Henzinger TA, Kueffner K. 2026. Energy shields for fairness.
Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency.
FAccT: Conference on Fairness, Accountability and Transparency, 4243–4275.'
mla: Cano Cordoba, Filip, et al. “Energy Shields for Fairness.” Proceedings of
the 2026 ACM Conference on Fairness, Accountability, and Transparency, Association
for Computing Machinery, 2026, pp. 4243–75, doi:10.1145/3805689.3806807.
short: F. Cano Cordoba, T.A. Henzinger, K. Kueffner, in:, Proceedings of the 2026
ACM Conference on Fairness, Accountability, and Transparency, Association for
Computing Machinery, 2026, pp. 4243–4275.
conference:
end_date: 2026-06-28
location: Montreal, Canada
name: 'FAccT: Conference on Fairness, Accountability and Transparency'
start_date: 2026-06-25
corr_author: '1'
das_tickbox: '0'
date_created: 2026-07-14T05:32:45Z
date_published: 2026-07-01T00:00:00Z
date_updated: 2026-07-22T06:15:56Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3805689.3806807
ec_funded: 1
external_id:
arxiv:
- '2605.24926'
file:
- access_level: open_access
checksum: 21e648ea3b529f0df7545ad4b31b0ef4
content_type: application/pdf
creator: dernst
date_created: 2026-07-16T09:23:15Z
date_updated: 2026-07-16T09:23:15Z
file_id: '22348'
file_name: 2026_ACMFACCT_Cano.pdf
file_size: 3129128
relation: main_file
success: 1
file_date_updated: 2026-07-16T09:23:15Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 4243 - 4275
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 2026 ACM Conference on Fairness, Accountability, and
Transparency
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: yes
title: Energy shields for 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
year: '2026'
...
---
OA_place: publisher
OA_type: gold
_id: '22617'
abstract:
- lang: eng
text: "Consider a 4-player version of Matching Pennies where a team of three players
competes against the Devil. Each player simultaneously says \"Heads\" or \"Tails\".
The team wins if all four choices match; otherwise the Devil wins. If all team
players randomise independently, they win with probability 1/8; if all players
share a common source of randomness, they win with probability 1/2. What happens
when each pair of team players shares a source of randomness? Can the team do
better than win with probability 1/4? The surprising (and nontrivial) answer is
yes!\r\nWe introduce Dicey Games, a formal framework motivated by the study of
distributed systems with shared sources of randomness (of which the above example
is a specific instance). We characterise the existence, representation and computational
complexity of optimal strategies in Dicey Games, and we study the problem of allocating
limited sources of randomness optimally within a team."
acknowledgement: "This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS).\r\nLéonard
Brice: Part of this work was realised when this author was an FNRS aspirant at Université
libre de Bruxelles.\r\nK. S. Thejaswini: Part of this work was realised when this
author was a post-doctoral researcher at IST Austria.\r\nAcknowledgements We thank
all our colleagues who took the time to hear our puzzle and wasted several hours
of their research time in pursuit of the optimal bounds for the 3-player matching.\r\npennies
problem.\r\n"
alternative_title:
- LIPIcs
article_number: 23:1-23:26
article_processing_charge: No
arxiv: 1
author:
- first_name: Leonard J
full_name: Brice, Leonard J
id: ce3b3409-db6c-11f0-aa64-ad678f7fd937
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.
last_name: Thejaswini
citation:
ama: 'Brice LJ, Henzinger TA, Thejaswini KS. Dicey games: Shared sources of randomness
in distributed systems. In: 41st Annual Symposium on Logic in Computer Science.
Vol 380. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:10.4230/LIPIcs.LICS.2026.23'
apa: 'Brice, L. J., Henzinger, T. A., & Thejaswini, K. S. (2026). Dicey games:
Shared sources of randomness in distributed systems. In 41st Annual Symposium
on Logic in Computer Science (Vol. 380). Lisbon, Portugal: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.LICS.2026.23'
chicago: 'Brice, Leonard J, Thomas A Henzinger, and K. S. Thejaswini. “Dicey Games:
Shared Sources of Randomness in Distributed Systems.” In 41st Annual Symposium
on Logic in Computer Science, Vol. 380. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2026. https://doi.org/10.4230/LIPIcs.LICS.2026.23.'
ieee: 'L. J. Brice, T. A. Henzinger, and K. S. Thejaswini, “Dicey games: Shared
sources of randomness in distributed systems,” in 41st Annual Symposium on
Logic in Computer Science, Lisbon, Portugal, 2026, vol. 380.'
ista: 'Brice LJ, Henzinger TA, Thejaswini KS. 2026. Dicey games: Shared sources
of randomness in distributed systems. 41st Annual Symposium on Logic in Computer
Science. LICS: Logic in Computer Science, LIPIcs, vol. 380, 23:1-23:26.'
mla: 'Brice, Leonard J., et al. “Dicey Games: Shared Sources of Randomness in Distributed
Systems.” 41st Annual Symposium on Logic in Computer Science, vol. 380,
23:1-23:26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:10.4230/LIPIcs.LICS.2026.23.'
short: L.J. Brice, T.A. Henzinger, K.S. Thejaswini, in:, 41st Annual Symposium on
Logic in Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2026.
conference:
end_date: 2026-07-23
location: Lisbon, Portugal
name: 'LICS: Logic in Computer Science'
start_date: 2026-07-20
corr_author: '1'
das_tickbox: '0'
date_created: 2026-08-02T22:01:52Z
date_published: 2026-07-09T00:00:00Z
date_updated: 2026-08-03T07:03:28Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.LICS.2026.23
ec_funded: 1
external_id:
arxiv:
- '2601.18303'
file:
- access_level: open_access
checksum: 5d0ff4d267565188a8b4c7502e1bd243
content_type: application/pdf
creator: dernst
date_created: 2026-08-03T07:02:30Z
date_updated: 2026-08-03T07:02:30Z
file_id: '22625'
file_name: 2026_LIPICSLICS_Brice.pdf
file_size: 919708
relation: main_file
success: 1
file_date_updated: 2026-08-03T07:02:30Z
has_accepted_license: '1'
intvolume: ' 380'
keyword:
- Concurrent games
- Shared randomness
- Topology
- Algebraic Geometry
language:
- iso: eng
month: '07'
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: 41st Annual Symposium on Logic in Computer Science
publication_identifier:
isbn:
- '9783959774345'
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'Dicey games: Shared sources of randomness in distributed systems'
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: 380
year: '2026'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '22406'
abstract:
- lang: eng
text: "It is known that for a uniform morphic sequence \U0001D496 =⟨\U0001D462\U0001D45B⟩∞\r\n\U0001D45B=0
and an algebraic number \U0001D6FD such that |\U0001D6FD| >1, the number [[\U0001D496]]\U0001D6FD
:=∑∞\r\n\U0001D45B=0(\U0001D462\U0001D45B/\U0001D6FD\U0001D45B) either lies in
ℚ(\U0001D6FD) or is transcendental. In this paper, we show a similar rational–transcendental
dichotomy for sequences defined by irreducible Pisot morphisms on binary alphabets.
Subject to the Pisot conjecture (an irreducible Pisot morphism has pure discrete
spectrum), we generalise the latter result to arbitrary finite alphabets. In certain
cases, we are able to show transcendence of [[\U0001D496]]\U0001D6FD outright.
In particular, for \U0001D458 ≥2, if \U0001D496 is the k-Bonacci word, then [[\U0001D496]]\U0001D6FD
is transcendental."
acknowledgement: "We thank the anonymous referee for identifying an error in an earlier\r\nversion
of the paper. We gratefully acknowledge support from UKRI Frontier Research\r\nGrant
EP/X033813/1, ERC grant DynAMiCS (101167561) and DFG grant 389792660 as\r\npart
of TRR 248. J.O. is also affiliated with Keble College, Oxford as an Emmy Network\r\nfellow."
article_processing_charge: Yes (in subscription journal)
article_type: original
arxiv: 1
author:
- first_name: Pavol
full_name: Kebis, Pavol
id: 2e0132b3-4e98-11ef-b275-cf7281c2802a
last_name: Kebis
- first_name: FLORIAN
full_name: LUCA, FLORIAN
last_name: LUCA
- first_name: JOEL
full_name: OUAKNINE, JOEL
last_name: OUAKNINE
- first_name: ANDREW
full_name: SCOONES, ANDREW
last_name: SCOONES
- first_name: JAMES
full_name: WORRELL, JAMES
last_name: WORRELL
citation:
ama: Kebis P, LUCA F, OUAKNINE J, SCOONES A, WORRELL J. Transcendence for Pisot
morphic words over an algebraic base. Ergodic Theory and Dynamical Systems.
2026:1-22. doi:10.1017/etds.2026.10324
apa: Kebis, P., LUCA, F., OUAKNINE, J., SCOONES, A., & WORRELL, J. (2026). Transcendence
for Pisot morphic words over an algebraic base. Ergodic Theory and Dynamical
Systems. Cambridge University Press. https://doi.org/10.1017/etds.2026.10324
chicago: Kebis, Pavol, FLORIAN LUCA, JOEL OUAKNINE, ANDREW SCOONES, and JAMES WORRELL.
“Transcendence for Pisot Morphic Words over an Algebraic Base.” Ergodic Theory
and Dynamical Systems. Cambridge University Press, 2026. https://doi.org/10.1017/etds.2026.10324.
ieee: P. Kebis, F. LUCA, J. OUAKNINE, A. SCOONES, and J. WORRELL, “Transcendence
for Pisot morphic words over an algebraic base,” Ergodic Theory and Dynamical
Systems. Cambridge University Press, pp. 1–22, 2026.
ista: Kebis P, LUCA F, OUAKNINE J, SCOONES A, WORRELL J. 2026. Transcendence for
Pisot morphic words over an algebraic base. Ergodic Theory and Dynamical Systems.,
1–22.
mla: Kebis, Pavol, et al. “Transcendence for Pisot Morphic Words over an Algebraic
Base.” Ergodic Theory and Dynamical Systems, Cambridge University Press,
2026, pp. 1–22, doi:10.1017/etds.2026.10324.
short: P. Kebis, F. LUCA, J. OUAKNINE, A. SCOONES, J. WORRELL, Ergodic Theory and
Dynamical Systems (2026) 1–22.
das_tickbox: '0'
date_created: 2026-07-27T05:53:25Z
date_published: 2026-07-10T00:00:00Z
date_updated: 2026-08-03T06:17:50Z
day: '10'
ddc:
- '000'
department:
- _id: ToHe
- _id: GradSch
doi: 10.1017/etds.2026.10324
external_id:
arxiv:
- '2405.05279'
has_accepted_license: '1'
keyword:
- balanced-pair algorithm
- Cobham’s conjecture
- k-Bonacci words
- Pisot conjecture
- subspace theorem
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1017/etds.2026.10324
mathsc:
- 11J81
- 37B10
- 11J87
month: '07'
oa: 1
oa_version: Published Version
page: 1-22
publication: Ergodic Theory and Dynamical Systems
publication_identifier:
eissn:
- 1469-4417
issn:
- 0143-3857
publication_status: epub_ahead
publisher: Cambridge University Press
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Transcendence for Pisot morphic words over an algebraic base
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
year: '2026'
...
---
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'
...
---
OA_place: publisher
OA_type: hybrid
_id: '21020'
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\nIn
this work, we propose two novel protocols for the privacy-preserving runtime verification
of systems against formal sequential specifications. In our first protocol, the
monitor verifies whether the system satisfies the specification without learning
anything else, though both parties are aware of the specification. Our second
protocol ensures that the system remains oblivious to the monitored specification,
while the monitor learns only whether the system satisfies the specification and
nothing more. Our protocols adapt and improve existing techniques used in cryptography,
and more specifically, multi-party computation.\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 protocols exchange
a single message per observation step, after an initialisation phase. This design
minimises communication overhead, enabling relatively lightweight privacy-preserving
monitoring. We implement our approach for monitoring specifications described
by register automata and evaluate it experimentally."
acknowledgement: This work is a part of projects VAMOS that has received fund-ing
from the European Research Council (ERC), grant agreementNo 101020093 and the Austrian
Science Fund (FWF) SFB projectSpyCoDe F8502.We thank anonymous reviewers for pointing
us to related work [ 3] and for their valuable suggestions that improved this paper.
article_processing_charge: Yes (via OA deal)
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: Mahyar
full_name: Karimi, Mahyar
id: 6e5417ba-5355-11ee-ae5a-94c2e510b26b
last_name: Karimi
orcid: 0009-0005-0820-1696
- first_name: K. S.
full_name: Thejaswini, K. S.
id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
last_name: Thejaswini
citation:
ama: 'Henzinger TA, Karimi M, Thejaswini KS. Privacy-preserving runtime verification.
In: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications
Security. Association for Computing Machinery; 2025:2774-2787. doi:10.1145/3719027.3765137'
apa: 'Henzinger, T. A., Karimi, M., & Thejaswini, K. S. (2025). Privacy-preserving
runtime verification. In Proceedings of the 2025 ACM SIGSAC Conference on Computer
and Communications Security (pp. 2774–2787). Taipei, Taiwan: Association for
Computing Machinery. https://doi.org/10.1145/3719027.3765137'
chicago: Henzinger, Thomas A, Mahyar Karimi, and K. S. Thejaswini. “Privacy-Preserving
Runtime Verification.” In Proceedings of the 2025 ACM SIGSAC Conference on
Computer and Communications Security, 2774–87. Association for Computing Machinery,
2025. https://doi.org/10.1145/3719027.3765137.
ieee: T. A. Henzinger, M. Karimi, and K. S. Thejaswini, “Privacy-preserving runtime
verification,” in Proceedings of the 2025 ACM SIGSAC Conference on Computer
and Communications Security, Taipei, Taiwan, 2025, pp. 2774–2787.
ista: 'Henzinger TA, Karimi M, Thejaswini KS. 2025. Privacy-preserving runtime verification.
Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security.
CCS: Conference on Computer and Communications Security, 2774–2787.'
mla: Henzinger, Thomas A., et al. “Privacy-Preserving Runtime Verification.” Proceedings
of the 2025 ACM SIGSAC Conference on Computer and Communications Security,
Association for Computing Machinery, 2025, pp. 2774–87, doi:10.1145/3719027.3765137.
short: T.A. Henzinger, M. Karimi, K.S. Thejaswini, in:, Proceedings of the 2025
ACM SIGSAC Conference on Computer and Communications Security, Association for
Computing Machinery, 2025, pp. 2774–2787.
conference:
end_date: 2025-10-17
location: Taipei, Taiwan
name: 'CCS: Conference on Computer and Communications Security'
start_date: 2025-10-13
corr_author: '1'
date_created: 2026-01-20T10:17:10Z
date_published: 2025-11-22T00:00:00Z
date_updated: 2026-03-13T13:37:19Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
- _id: GradSch
doi: 10.1145/3719027.3765137
ec_funded: 1
external_id:
arxiv:
- '2505.09276'
file:
- access_level: open_access
checksum: 615ffddab6c7285158c2953acec6fa6f
content_type: application/pdf
creator: dernst
date_created: 2026-01-21T07:34:58Z
date_updated: 2026-01-21T07:34:58Z
file_id: '21024'
file_name: 2025_CCS_HenzingerT.pdf
file_size: 1241912
relation: main_file
success: 1
file_date_updated: 2026-01-21T07:34:58Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
page: 2774-2787
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: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications
Security
publication_identifier:
isbn:
- '9798400715259'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '21401'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Privacy-preserving runtime 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
year: '2025'
...
---
OA_place: publisher
OA_type: gold
_id: '21089'
abstract:
- lang: eng
text: 'Hypertrace logic is a sorted first-order logic with separate sorts for time
and execution traces. Its formulas specify hyperproperties, which are properties
relating multiple traces. In this work, we extend hypertrace logic by introducing
trace quantifiers that range over the set of all possible traces. In this extended
logic, formulas can quantify over two kinds of trace variables: constrained trace
variables, which range over a fixed set of traces defined by the model, and unconstrained
trace variables, which can be assigned to any trace. In comparison, hyperlogics
such as HyperLTL have only constrained trace quantifiers. We use hypertrace logic
to study how different quantifier patterns affect the decidability of the satisfiability
problem. We prove that hypertrace logic without constrained trace quantifiers
is equivalent to monadic second-order logic of one successor (S1S), and therefore
satisfiable, and that the trace-prefixed fragment (all trace quantifiers precede
all time quantifiers) is equivalent to HyperQPTL. Moreover, we show that all hypertrace
formulas where the only alternation between constrained trace quantifiers is from
an existential to a universal quantifier are equisatisfiable to formulas without
constraints on their trace variables and, therefore, decidable as well. Our framework
allows us to study also time-prefixed hyperlogics, for which we provide new decidability
and undecidability results.'
acknowledgement: This work was supported in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe 10.55776/F85 and by the ERC Advanced Grant VAMOS 101020093.
alternative_title:
- LIPIcs
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Ana A
full_name: Oliveira da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira da Costa
citation:
ama: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. Flavors of quantifiers in hyperlogics.
In: 45th Annual Conference on Foundations of Software Technology and Theoretical
Computer Science. Vol 360. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
2025:20:1-20:18. doi:10.4230/LIPICS.FSTTCS.2025.20'
apa: 'Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. A. (2025). Flavors
of quantifiers in hyperlogics. In 45th Annual Conference on Foundations of
Software Technology and Theoretical Computer Science (Vol. 360, p. 20:1-20:18).
Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.FSTTCS.2025.20'
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Flavors
of Quantifiers in Hyperlogics.” In 45th Annual Conference on Foundations of
Software Technology and Theoretical Computer Science, 360:20:1-20:18. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2025. https://doi.org/10.4230/LIPICS.FSTTCS.2025.20.
ieee: M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Flavors of quantifiers
in hyperlogics,” in 45th Annual Conference on Foundations of Software Technology
and Theoretical Computer Science, Pilani, India, 2025, vol. 360, p. 20:1-20:18.
ista: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Flavors of quantifiers
in hyperlogics. 45th Annual Conference on Foundations of Software Technology and
Theoretical Computer Science. FSTTCS: Conference on Foundations of Software Technology
and Theoretical Computer Science, LIPIcs, vol. 360, 20:1-20:18.'
mla: Chalupa, Marek, et al. “Flavors of Quantifiers in Hyperlogics.” 45th Annual
Conference on Foundations of Software Technology and Theoretical Computer Science,
vol. 360, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18,
doi:10.4230/LIPICS.FSTTCS.2025.20.
short: M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 45th Annual Conference
on Foundations of Software Technology and Theoretical Computer Science, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18.
conference:
end_date: 2025-12-19
location: Pilani, India
name: 'FSTTCS: Conference on Foundations of Software Technology and Theoretical
Computer Science'
start_date: 2025-12-17
corr_author: '1'
date_created: 2026-01-29T15:39:15Z
date_published: 2025-12-09T00:00:00Z
date_updated: 2026-02-11T09:35:04Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPICS.FSTTCS.2025.20
ec_funded: 1
external_id:
arxiv:
- '2510.12298'
file:
- access_level: open_access
checksum: 8188ee5c7b14193d48eeb655e9bbdc47
content_type: application/pdf
creator: dernst
date_created: 2026-02-11T09:33:20Z
date_updated: 2026-02-11T09:33:20Z
file_id: '21213'
file_name: 2025_LIPIcS_Chalupa.pdf
file_size: 933970
relation: main_file
success: 1
file_date_updated: 2026-02-11T09:33:20Z
has_accepted_license: '1'
intvolume: ' 360'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: 20:1-20:18
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: 45th Annual Conference on Foundations of Software Technology and Theoretical
Computer Science
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Flavors of quantifiers in hyperlogics
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: 360
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '21090'
abstract:
- lang: eng
text: Fairness in AI is traditionally studied as a static property evaluated once,
over a fixed dataset. However, real-world AI systems operate sequentially, with
outcomes and environments evolving over time. This paper proposes a framework
for analysing fairness as a runtime property. Using a minimal yet expressive model
based on sequences of coin tosses with possibly evolving biases, we study the
problems of monitoring and enforcing fairness expressed in either toss outcomes
or coin biases. Since there is no one-size-fits-all solution for either problem,
we provide a summary of monitoring and enforcement strategies, parametrised by
environment dynamics, prediction horizon, and confidence thresholds. For both
problems, we present general results under simple or minimal assumptions. We survey
existing solutions for the monitoring problem for Markovian and additive dynamics,
and existing solutions for the enforcement problem in static settings with known
dynamics.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG 101020093.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: 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: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
citation:
ama: 'Cano Cordoba F, Henzinger TA, Kueffner K. Algorithmic fairness: A runtime
perspective. In: 25th International Conference on Runtime Verification.
Vol 16087. Springer Nature; 2025:1-21. doi:10.1007/978-3-032-05435-7_1'
apa: 'Cano Cordoba, F., Henzinger, T. A., & Kueffner, K. (2025). Algorithmic
fairness: A runtime perspective. In 25th International Conference on Runtime
Verification (Vol. 16087, pp. 1–21). Graz, Austria: Springer Nature. https://doi.org/10.1007/978-3-032-05435-7_1'
chicago: 'Cano Cordoba, Filip, Thomas A Henzinger, and Konstantin Kueffner. “Algorithmic
Fairness: A Runtime Perspective.” In 25th International Conference on Runtime
Verification, 16087:1–21. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05435-7_1.'
ieee: 'F. Cano Cordoba, T. A. Henzinger, and K. Kueffner, “Algorithmic fairness:
A runtime perspective,” in 25th International Conference on Runtime Verification,
Graz, Austria, 2025, vol. 16087, pp. 1–21.'
ista: 'Cano Cordoba F, Henzinger TA, Kueffner K. 2025. Algorithmic fairness: A runtime
perspective. 25th International Conference on Runtime Verification. RV: Runtime
Verification, LNCS, vol. 16087, 1–21.'
mla: 'Cano Cordoba, Filip, et al. “Algorithmic Fairness: A Runtime Perspective.”
25th International Conference on Runtime Verification, vol. 16087, Springer
Nature, 2025, pp. 1–21, doi:10.1007/978-3-032-05435-7_1.'
short: F. Cano Cordoba, T.A. Henzinger, K. Kueffner, in:, 25th International Conference
on Runtime Verification, Springer Nature, 2025, pp. 1–21.
conference:
end_date: 2025-09-19
location: Graz, Austria
name: 'RV: Runtime Verification'
start_date: 2025-09-15
corr_author: '1'
date_created: 2026-01-29T16:01:41Z
date_published: 2025-09-13T00:00:00Z
date_updated: 2026-02-16T11:57:00Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-032-05435-7_1
ec_funded: 1
external_id:
arxiv:
- '2507.20711'
intvolume: ' 16087'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2507.20711
month: '09'
oa: 1
oa_version: Preprint
page: 1-21
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 25th International Conference on Runtime Verification
publication_identifier:
eisbn:
- '9783032054357'
eissn:
- 1611-3349
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: 'Algorithmic fairness: A runtime perspective'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16087
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '21091'
abstract:
- lang: eng
text: Neural certificates have emerged as a powerful tool in cyber-physical systems
control, providing witnesses of correctness. These certificates, such as barrier
functions, often learned alongside control policies, once verified, serve as mathematical
proofs of system safety. However, traditional formal verification of their defining
conditions typically faces scalability challenges due to exhaustive state-space
exploration. To address this challenge, we propose a lightweight runtime monitoring
framework that integrates real-time verification and does not require access to
the underlying control policy. Our monitor observes the system during deployment
and performs on-the-fly verification of the certificate over a lookahead region
to ensure safety within a finite prediction horizon. We instantiate this framework
for ReLU-based control barrier functions and demonstrate its practical effectiveness
in a case study. Our approach enables timely detection of safety violations and
incorrect certificates with minimal overhead, providing an effective but lightweight
alternative to the static verification of the certificates.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG 101020093.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
citation:
ama: 'Henzinger TA, Kueffner K, Yu E. Formal verification of neural certificates
done dynamically. In: 25th International Conference on Runtime Verification.
Vol 16087. Springer Nature; 2025:54-72. doi:10.1007/978-3-032-05435-7_4'
apa: 'Henzinger, T. A., Kueffner, K., & Yu, E. (2025). Formal verification of
neural certificates done dynamically. In 25th International Conference on Runtime
Verification (Vol. 16087, pp. 54–72). Graz, Austria: Springer Nature. https://doi.org/10.1007/978-3-032-05435-7_4'
chicago: Henzinger, Thomas A, Konstantin Kueffner, and Emily Yu. “Formal Verification
of Neural Certificates Done Dynamically.” In 25th International Conference
on Runtime Verification, 16087:54–72. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05435-7_4.
ieee: T. A. Henzinger, K. Kueffner, and E. Yu, “Formal verification of neural certificates
done dynamically,” in 25th International Conference on Runtime Verification,
Graz, Austria, 2025, vol. 16087, pp. 54–72.
ista: 'Henzinger TA, Kueffner K, Yu E. 2025. Formal verification of neural certificates
done dynamically. 25th International Conference on Runtime Verification. RV: Runtime
Verification, LNCS, vol. 16087, 54–72.'
mla: Henzinger, Thomas A., et al. “Formal Verification of Neural Certificates Done
Dynamically.” 25th International Conference on Runtime Verification, vol.
16087, Springer Nature, 2025, pp. 54–72, doi:10.1007/978-3-032-05435-7_4.
short: T.A. Henzinger, K. Kueffner, E. Yu, in:, 25th International Conference on
Runtime Verification, Springer Nature, 2025, pp. 54–72.
conference:
end_date: 2025-09-19
location: Graz, Austria
name: 'RV: Runtime Verification'
start_date: 2025-09-15
corr_author: '1'
date_created: 2026-01-29T16:03:01Z
date_published: 2025-09-13T00:00:00Z
date_updated: 2026-02-16T11:53:25Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-032-05435-7_4
ec_funded: 1
external_id:
arxiv:
- '2507.11987'
intvolume: ' 16087'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2507.11987
month: '09'
oa: 1
oa_version: Preprint
page: 54-72
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 25th International Conference on Runtime Verification
publication_identifier:
eisbn:
- '9783032054357'
eissn:
- 1611-3349
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Formal verification of neural certificates done dynamically
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16087
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '21092'
abstract:
- lang: eng
text: Formal verification provides assurances that a probabilistic system satisfies
its specification—conditioned on the system model being aligned with reality.
We propose alignment monitoring to watch that this assumption is justified. We
consider a probabilistic model well aligned if it accurately predicts the behaviour
of an uncertain system in advance. An alignment score measures this by quantifying
the similarity between the model’s predicted and the system’s (unknown) actual
distributions. An alignment monitor observes the system at runtime; at each point
in time it uses the current state and the model to predict the next state. After
the next state is observed, the monitor updates the verdict, which is a high-probability
interval estimate for the true alignment score. We utilize tools from sequential
forecasting to construct our alignment monitors. Besides a monitor for measuring
the expected alignment score, we introduce a differential alignment monitor, designed
for comparing two models, and a weighted alignment monitor, which permits task-specific
alignment monitoring. We evaluate our monitors experimentally on the PRISM benchmark
suite. They are fast, memory-efficient, and detect misalignment early.
acknowledgement: 'This work is supported by the European Research Council under Grant
No.: ERC-2020-AdG 101020093.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Konstantin
full_name: Kueffner, Konstantin
id: 8121a2d0-dc85-11ea-9058-af578f3b4515
last_name: Kueffner
orcid: 0000-0001-8974-2542
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
- first_name: I
full_name: Sun, I
last_name: Sun
citation:
ama: 'Henzinger TA, Kueffner K, Singh V, Sun I. Alignment monitoring. In: 25th
International Conference on Runtime Verification. Vol 16087. Springer Nature;
2025:140-159. doi:10.1007/978-3-032-05435-7_9'
apa: 'Henzinger, T. A., Kueffner, K., Singh, V., & Sun, I. (2025). Alignment
monitoring. In 25th International Conference on Runtime Verification (Vol.
16087, pp. 140–159). Graz, Austria: Springer Nature. https://doi.org/10.1007/978-3-032-05435-7_9'
chicago: Henzinger, Thomas A, Konstantin Kueffner, Vasu Singh, and I Sun. “Alignment
Monitoring.” In 25th International Conference on Runtime Verification,
16087:140–59. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05435-7_9.
ieee: T. A. Henzinger, K. Kueffner, V. Singh, and I. Sun, “Alignment monitoring,”
in 25th International Conference on Runtime Verification, Graz, Austria,
2025, vol. 16087, pp. 140–159.
ista: 'Henzinger TA, Kueffner K, Singh V, Sun I. 2025. Alignment monitoring. 25th
International Conference on Runtime Verification. RV: Runtime Verification, LNCS,
vol. 16087, 140–159.'
mla: Henzinger, Thomas A., et al. “Alignment Monitoring.” 25th International
Conference on Runtime Verification, vol. 16087, Springer Nature, 2025, pp.
140–59, doi:10.1007/978-3-032-05435-7_9.
short: T.A. Henzinger, K. Kueffner, V. Singh, I. Sun, in:, 25th International Conference
on Runtime Verification, Springer Nature, 2025, pp. 140–159.
conference:
end_date: 2025-09-19
location: Graz, Austria
name: 'RV: Runtime Verification'
start_date: 2025-09-15
corr_author: '1'
date_created: 2026-01-29T16:03:43Z
date_published: 2025-09-13T00:00:00Z
date_updated: 2026-02-16T11:56:38Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-032-05435-7_9
ec_funded: 1
external_id:
arxiv:
- '2508.00021'
intvolume: ' 16087'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2508.00021
month: '09'
oa: 1
oa_version: Preprint
page: 140-159
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 25th International Conference on Runtime Verification
publication_identifier:
eisbn:
- '9783032054357'
eissn:
- 1611-3349
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Alignment monitoring
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16087
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '21093'
abstract:
- lang: eng
text: We propose a monitoring approach for hyperproperties where the system’s observations
range over infinite domains. The specifications are given as formulas of symbolic
hypernode logic, an extension of earlier versions of hypernode logic that supports
events with data. We demonstrate how to translate terms of symbolic hypernode
logic into multi-tape symbolic transducers and we present a monitoring algorithm
for universally quantified formulas that is based on this translation. We evaluate
our approach against the previous approach for monitoring hypernode logic, and
we also compare it to other monitors for hyperproperties.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093 and
in part by the FWF-2022-SFB F8502 (SPyCoDe).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Ana A
full_name: Oliveira da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira da Costa
citation:
ama: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. Monitoring hypernode logic
over infinite domains. In: 25th International Conference on Runtime Verification.
Vol 16087. Springer Nature; 2025:417-437. doi:10.1007/978-3-032-05435-7_23'
apa: 'Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. A. (2025). Monitoring
hypernode logic over infinite domains. In 25th International Conference on
Runtime Verification (Vol. 16087, pp. 417–437). Graz, Austria: Springer Nature.
https://doi.org/10.1007/978-3-032-05435-7_23'
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Monitoring
Hypernode Logic over Infinite Domains.” In 25th International Conference on
Runtime Verification, 16087:417–37. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05435-7_23.
ieee: M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Monitoring hypernode
logic over infinite domains,” in 25th International Conference on Runtime Verification,
Graz, Austria, 2025, vol. 16087, pp. 417–437.
ista: 'Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Monitoring hypernode
logic over infinite domains. 25th International Conference on Runtime Verification.
RV: Runtime Verification, LNCS, vol. 16087, 417–437.'
mla: Chalupa, Marek, et al. “Monitoring Hypernode Logic over Infinite Domains.”
25th International Conference on Runtime Verification, vol. 16087, Springer
Nature, 2025, pp. 417–37, doi:10.1007/978-3-032-05435-7_23.
short: M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 25th International
Conference on Runtime Verification, Springer Nature, 2025, pp. 417–437.
conference:
end_date: 2025-09-19
location: Graz, Austria
name: 'RV: Runtime Verification'
start_date: 2025-09-15
corr_author: '1'
date_created: 2026-01-29T16:04:31Z
date_published: 2025-09-13T00:00:00Z
date_updated: 2026-02-16T11:59:20Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-032-05435-7_23
ec_funded: 1
external_id:
arxiv:
- '2508.02301'
intvolume: ' 16087'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2508.02301
month: '09'
oa: 1
oa_version: Preprint
page: 417-437
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: 25th International Conference on Runtime Verification
publication_identifier:
eisbn:
- '9783032054357'
eissn:
- 1611-3349
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Monitoring hypernode logic over infinite domains
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16087
year: '2025'
...
---
OA_type: closed access
_id: '21885'
abstract:
- lang: eng
text: Symbolic datatypes have proved to be central for automated reasoning about
dynamical systems. In its basic form, a symbolic datatype for a class of dynamical
systems supports the representation of state and transition sets, boolean operations
and emptiness checks on such sets, and the transformation of a state set by a
transition set. Successful examples of symbolic datatypes include BDDs and SAT
for reasoning about finitestate systems, as well as polyhedra and SMT for reasoning
about discrete dynamical systems over multidimensional realvalued state spaces.
Most automated verification engines are based on such symbolic datatypes.
article_processing_charge: No
author:
- 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: 'Henzinger TA. Neural Certificates. In: Proceedings of the 27th International
Symposium on Symbolic and Numeric Algorithms for Scientific Computing. IEEE;
2025. doi:10.1109/SYNASC69064.2025.00008'
apa: 'Henzinger, T. A. (2025). Neural Certificates. In Proceedings of the 27th
International Symposium on Symbolic and Numeric Algorithms for Scientific Computing.
Timisoara, Romania: IEEE. https://doi.org/10.1109/SYNASC69064.2025.00008'
chicago: Henzinger, Thomas A. “Neural Certificates.” In Proceedings of the 27th
International Symposium on Symbolic and Numeric Algorithms for Scientific Computing.
IEEE, 2025. https://doi.org/10.1109/SYNASC69064.2025.00008.
ieee: T. A. Henzinger, “Neural Certificates,” in Proceedings of the 27th International
Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara,
Romania, 2025.
ista: 'Henzinger TA. 2025. Neural Certificates. Proceedings of the 27th International
Symposium on Symbolic and Numeric Algorithms for Scientific Computing. SYNASC:
Symposium on Symbolic and Numeric Algorithms for Scientific Computing.'
mla: Henzinger, Thomas A. “Neural Certificates.” Proceedings of the 27th International
Symposium on Symbolic and Numeric Algorithms for Scientific Computing, IEEE,
2025, doi:10.1109/SYNASC69064.2025.00008.
short: T.A. Henzinger, in:, Proceedings of the 27th International Symposium on Symbolic
and Numeric Algorithms for Scientific Computing, IEEE, 2025.
conference:
end_date: 2025-09-25
location: Timisoara, Romania
name: 'SYNASC: Symposium on Symbolic and Numeric Algorithms for Scientific Computing'
start_date: 2025-09-22
corr_author: '1'
date_created: 2026-05-17T22:02:11Z
date_published: 2025-10-01T00:00:00Z
date_updated: 2026-05-18T08:34:15Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/SYNASC69064.2025.00008
language:
- iso: eng
month: '10'
oa_version: None
publication: Proceedings of the 27th International Symposium on Symbolic and Numeric
Algorithms for Scientific Computing
publication_identifier:
eisbn:
- '9798331590116'
eissn:
- 2470-881X
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Neural Certificates
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '17094'
abstract:
- lang: eng
text: Contract-based design is a promising methodology for taming the complexity
of developing sophisticated systems. A formal contract distinguishes between assumptions,
which are constraints that the designer of a component puts on the environments
in which the component can be used safely, and guarantees, which are promises
that the designer asks from the team that implements the component. A theory of
formal contracts can be formalized as an interface theory, which supports the
composition and refinement of both assumptions and guarantees. Although there
is a rich landscape of contract-based design methods that address functional and
extra-functional properties, we present the first interface theory designed to
ensure system-wide security properties. Our framework provides a refinement relation
and a composition operation that support both incremental design and independent
implementability. We develop our theory for both stateless and stateful interfaces.
Additionally, we introduce information-flow contracts where assumptions and guarantees
are sets of flow relations. We use these contracts to illustrate how to enrich
information-flow interfaces with a semantic view. We illustrate the applicability
of our framework with two examples inspired by the automotive domain.
acknowledgement: This project has received funding from the European Union’s Horizon
2020 research and innovation programme under grant agreement No 956123 and it was
funded in part by the Austrian Science Fund (FWF) project W1255-N23, by the Austrian
FWF project ZK-35, by the FWF project SpyCoDe 10.55776/F85 and by the ERC-2020-AdG
101020093. This paper extends the text and the results of the manuscript published
at FASE 2022 [1].
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: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- 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, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-flow
interfaces. Formal Methods in System Design. 2025;66:3-48. doi:10.1007/s10703-024-00447-0
apa: Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Oliveira da
Costa, A. (2025). Information-flow interfaces. Formal Methods in System Design.
Springer Nature. https://doi.org/10.1007/s10703-024-00447-0
chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira da Costa. “Information-Flow Interfaces.” Formal Methods in System
Design. Springer Nature, 2025. https://doi.org/10.1007/s10703-024-00447-0.
ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. Oliveira da
Costa, “Information-flow interfaces,” Formal Methods in System Design,
vol. 66. Springer Nature, pp. 3–48, 2025.
ista: Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.
Information-flow interfaces. Formal Methods in System Design. 66, 3–48.
mla: Bartocci, Ezio, et al. “Information-Flow Interfaces.” Formal Methods in
System Design, vol. 66, Springer Nature, 2025, pp. 3–48, doi:10.1007/s10703-024-00447-0.
short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa,
Formal Methods in System Design 66 (2025) 3–48.
corr_author: '1'
date_created: 2024-06-02T22:00:57Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-12-30T06:50:51Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s10703-024-00447-0
ec_funded: 1
external_id:
arxiv:
- '2002.06465'
isi:
- '001230084200001'
file:
- access_level: open_access
checksum: 244a71a916103b8ea08e9d0bab32bcd9
content_type: application/pdf
creator: dernst
date_created: 2025-12-30T06:50:12Z
date_updated: 2025-12-30T06:50:12Z
file_id: '20879'
file_name: 2025_FormalMethodsSysDesign_Bartocci.pdf
file_size: 3860690
relation: main_file
success: 1
file_date_updated: 2025-12-30T06:50:12Z
has_accepted_license: '1'
intvolume: ' 66'
isi: 1
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 3-48
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: Formal Methods in System Design
publication_identifier:
eissn:
- 1572-8102
issn:
- 0925-9856
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '11355'
relation: shorter_version
status: public
scopus_import: '1'
status: public
title: Information-flow interfaces
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: 66
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19499'
abstract:
- lang: eng
text: Quantum hardware is inherently fragile and noisy. We find that the accuracy
of traditional quantum error correction algorithms can be improved depending on
the hardware. Given different hardware specifications, we automatically synthesize
hardware-optimal algorithms for parity correction, qubit resetting, and GHZ (Greenberger–Horne–Zeilinger)
state preparation. Using stochastic techniques from computer science, our method
presents a computational tool to compute exact accuracy guarantees and synthesize
optimal algorithms that are often different from traditional ones. We also show
that improvements can be gained with respect to the Qiskit transpiler as we compute
the hardware-optimal qubit mapping for the GHZ state-preparation problem.
acknowledgement: We thank the reviewers. In particular, they inspired us to analyze
the reset and state-preparation problems, to compute optimal qubit mappings, and
to apply our method to a quantum error correction scheme that includes both bitflip
and phaseflip corrections. We also thank Raimundo Saona and Marek Chalupa for their
time spent in insightful discussions. This research was partially supported by the
European Research Council CoG 863818 (ForM-SMArt) grant.
article_number: e2419273122
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Muroya Lei S, Chatterjee K, Henzinger TA. Hardware-optimal quantum algorithms.
Proceedings of the National Academy of Sciences. 2025;122(12). doi:10.1073/pnas.2419273122
apa: Muroya Lei, S., Chatterjee, K., & Henzinger, T. A. (2025). Hardware-optimal
quantum algorithms. Proceedings of the National Academy of Sciences. National
Academy of Sciences. https://doi.org/10.1073/pnas.2419273122
chicago: Muroya Lei, Stefanie, Krishnendu Chatterjee, and Thomas A Henzinger. “Hardware-Optimal
Quantum Algorithms.” Proceedings of the National Academy of Sciences. National
Academy of Sciences, 2025. https://doi.org/10.1073/pnas.2419273122.
ieee: S. Muroya Lei, K. Chatterjee, and T. A. Henzinger, “Hardware-optimal quantum
algorithms,” Proceedings of the National Academy of Sciences, vol. 122,
no. 12. National Academy of Sciences, 2025.
ista: Muroya Lei S, Chatterjee K, Henzinger TA. 2025. Hardware-optimal quantum algorithms.
Proceedings of the National Academy of Sciences. 122(12), e2419273122.
mla: Muroya Lei, Stefanie, et al. “Hardware-Optimal Quantum Algorithms.” Proceedings
of the National Academy of Sciences, vol. 122, no. 12, e2419273122, National
Academy of Sciences, 2025, doi:10.1073/pnas.2419273122.
short: S. Muroya Lei, K. Chatterjee, T.A. Henzinger, Proceedings of the National
Academy of Sciences 122 (2025).
corr_author: '1'
date_created: 2025-04-06T22:01:32Z
date_published: 2025-03-25T00:00:00Z
date_updated: 2026-04-28T13:41:14Z
day: '25'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1073/pnas.2419273122
ec_funded: 1
external_id:
isi:
- '001459435600001'
pmid:
- '40106357'
file:
- access_level: open_access
checksum: 83501b8a65ee5fdd3f5604fc28eddc22
content_type: application/pdf
creator: dernst
date_created: 2025-04-07T11:42:22Z
date_updated: 2025-04-07T11:42:22Z
file_id: '19524'
file_name: 2025_PNAS_Muroya.pdf
file_size: 6805668
relation: main_file
success: 1
file_date_updated: 2025-04-07T11:42:22Z
has_accepted_license: '1'
intvolume: ' 122'
isi: 1
issue: '12'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '03'
oa: 1
oa_version: Published Version
pmid: 1
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the National Academy of Sciences
publication_identifier:
eissn:
- 1091-6490
issn:
- 0027-8424
publication_status: published
publisher: National Academy of Sciences
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/smml1996/algorithm_synthesis
- description: News on ISTA website
relation: press_release
url: https://ista.ac.at/en/news/hardware-optimal-quantum-algorithms/
scopus_import: '1'
status: public
title: Hardware-optimal quantum algorithms
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 122
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'
...