---
OA_place: publisher
OA_type: hybrid
_id: '19743'
abstract:
- lang: eng
text: The possibility of errors in human-engineered formal verification software,
such as model checkers, poses a serious threat to the purpose of these tools.
An established approach to mitigate this problem are certificates—lightweight,
easy-to-check proofs of the verification results. In this paper, we develop novel
certificates for model checking of Markov decision processes (MDPs) with quantitative
reachability and expected reward properties. Our approach is conceptually simple
and relies almost exclusively on elementary fixed point theory. Our certificates
work for arbitrary finite MDPs and can be readily computed with little overhead
using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL
and provide a formally verified certificate checker. Moreover, we augment existing
algorithms in the probabilistic model checker Storm with the ability to produce
certificates and demonstrate practical applicability by conducting the first formal
certification of the reference results in the Quantitative Verification Benchmark
Set.
acknowledgement: This project has received funding from the ERC CoG 863818 (ForM-SMArt),
the Austrian Science Fund (FWF) 10.55776/COE12, a KI-Starter grant from the Ministerium
für Kultur und Wissenschaft NRW, the DFG RTG 378803395 (ConVeY), the EU’s Horizon
2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement
Nos. 101034413 (IST-BRIDGE) and 101008233 (MISSION), and the DFG RTG 2236 (UnRAVeL).
Experiments were performed with computing resources granted by RWTH Aachen University
under project rwth1632.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Tim
full_name: Quatmann, Tim
last_name: Quatmann
- first_name: Maximilian
full_name: Schäffeler, Maximilian
last_name: Schäffeler
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
- first_name: Tobias
full_name: Winkler, Tobias
last_name: Winkler
- first_name: Daniel
full_name: Zilken, Daniel
id: d8ebc24a-3f98-11f0-9044-8296d4f39ab3
last_name: Zilken
citation:
ama: 'Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D.
Fixed point certificates for reachability and expected rewards in MDPs. In: 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. Vol 15697. Springer Nature; 2025:130-151. doi:10.1007/978-3-031-90653-4_7'
apa: 'Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T.,
& Zilken, D. (2025). Fixed point certificates for reachability and expected
rewards in MDPs. In 31st International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (Vol. 15697, pp. 130–151). Hamilton,
ON, Canada: Springer Nature. https://doi.org/10.1007/978-3-031-90653-4_7'
chicago: Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian
Weininger, Tobias Winkler, and Daniel Zilken. “Fixed Point Certificates for Reachability
and Expected Rewards in MDPs.” In 31st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, 15697:130–51. Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-90653-4_7.
ieee: K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D.
Zilken, “Fixed point certificates for reachability and expected rewards in MDPs,”
in 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Hamilton, ON, Canada, 2025, vol. 15697, pp. 130–151.
ista: 'Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D.
2025. Fixed point certificates for reachability and expected rewards in MDPs.
31st International Conference on Tools and Algorithms for the Construction and
Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, LNCS, vol. 15697, 130–151.'
mla: Chatterjee, Krishnendu, et al. “Fixed Point Certificates for Reachability and
Expected Rewards in MDPs.” 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, vol. 15697, Springer Nature,
2025, pp. 130–51, doi:10.1007/978-3-031-90653-4_7.
short: K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken,
in:, 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2025, pp. 130–151.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:09Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T10:55:34Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90653-4_7
ec_funded: 1
external_id:
arxiv:
- '2501.11467'
file:
- access_level: open_access
checksum: 64b7f46ef05649b87b827248045c7645
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T10:49:52Z
date_updated: 2025-06-02T10:49:52Z
file_id: '19772'
file_name: 2025_TACAS_ChatterjeeKrish.pdf
file_size: 732136
relation: main_file
success: 1
file_date_updated: 2025-06-02T10:49:52Z
has_accepted_license: '1'
intvolume: ' 15697'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 130-151
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906527'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '19771'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Fixed point certificates for reachability and expected rewards in MDPs
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: 15697
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19744'
abstract:
- lang: eng
text: We consider the problem of refuting equivalence of probabilistic programs,
i.e., the problem of proving that two probabilistic programs induce different
output distributions. We study this problem in the context of programs with conditioning
(i.e., with observe and score statements), where the output distribution is conditioned
by the event that all the observe statements along a run evaluate to true, and
where the probability densities of different runs may be updated via the score
statements. Building on a recent work on programs without conditioning, we present
a new equivalence refutation method for programs with conditioning. Our method
is based on weighted restarting, a novel transformation of probabilistic programs
with conditioning to the output equivalent probabilistic programs without conditioning
that we introduce in this work. Our method is the first to be both a) fully automated,
and b) providing provably correct answers. We demonstrate the applicability of
our method on a set of programs from the probabilistic inference literature.
acknowledgement: This work was partially supported by ERC CoG 863818 (ForM-SMArt)
and Austrian Science Fund (FWF) 10.55776/COE12. Petr Novotný is supported by the
Czech Science Foundation grant no. GA23-06963S.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ehsan
full_name: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Petr
full_name: Novotný, Petr
id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
last_name: Novotný
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady E, Novotný P, Zikelic D. Refuting equivalence in
probabilistic programs with conditioning. In: 31st International Conference
on Tools and Algorithms for the Construction and Analysis of Systems. Vol
15697. Springer Nature; 2025:279-300. doi:10.1007/978-3-031-90653-4_14'
apa: 'Chatterjee, K., Goharshady, E., Novotný, P., & Zikelic, D. (2025). Refuting
equivalence in probabilistic programs with conditioning. In 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 15697, pp. 279–300). Hamilton, ON, Canada: Springer Nature. https://doi.org/10.1007/978-3-031-90653-4_14'
chicago: Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic.
“Refuting Equivalence in Probabilistic Programs with Conditioning.” In 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, 15697:279–300. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-90653-4_14.
ieee: K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Refuting equivalence
in probabilistic programs with conditioning,” in 31st International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, Hamilton,
ON, Canada, 2025, vol. 15697, pp. 279–300.
ista: 'Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2025. Refuting equivalence
in probabilistic programs with conditioning. 31st International Conference on
Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697,
279–300.'
mla: Chatterjee, Krishnendu, et al. “Refuting Equivalence in Probabilistic Programs
with Conditioning.” 31st International Conference on Tools and Algorithms for
the Construction and Analysis of Systems, vol. 15697, Springer Nature, 2025,
pp. 279–300, doi:10.1007/978-3-031-90653-4_14.
short: K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, in:, 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Springer Nature, 2025, pp. 279–300.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:10Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T11:16:13Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90653-4_14
ec_funded: 1
external_id:
arxiv:
- '2501.06579'
file:
- access_level: open_access
checksum: 7dcd85e7e753bfa994c10b3cf9ebc185
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T11:13:49Z
date_updated: 2025-06-02T11:13:49Z
file_id: '19773'
file_name: 2025_TACAS_Chatterjee_Goharshadi.pdf
file_size: 532181
relation: main_file
success: 1
file_date_updated: 2025-06-02T11:13:49Z
has_accepted_license: '1'
intvolume: ' 15697'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 279-300
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906527'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Refuting equivalence in probabilistic programs with conditioning
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: 15697
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20844'
abstract:
- lang: eng
text: "We introduce and construct a new proof system called Non-interactive Arguments
of Knowledge or Space (NArKoS), where a space-bounded prover can convince a verifier
they know a secret, while having access to sufficient space allows one to forge
indistinguishable proofs without the secret.\r\nAn application of NArKoS are space-deniable
proofs, which are proofs of knowledge (say for authentication in access control)
that are sound when executed by a lightweight device like a smart-card or an RFID
chip that cannot have much storage, but are deniable (in the strong sense of online
deniability) as the verifier, like a card reader, can efficiently forge such proofs.\r\nWe
construct NArKoS in the random oracle model using an OR-proof combining a sigma
protocol (for the proof of knowledge of the secret) with a new proof system called
simulatable Proof of Transient Space (simPoTS). We give two different constructions
of simPoTS, one based on labelling graphs with high pebbling complexity, a technique
used in the construction of memory-hard functions and proofs of space, and a more
practical construction based on the verifiable space-hard functions from TCC’24
where a prover must compute a root of a sparse polynomial. In both cases, the
main challenge is making the proofs efficiently simulatable."
acknowledgement: "Jesko Dujmovic: Funded by the European Union (ERC, LACONIC, 101041207).
Views and opinions expressed are however those of the author(s) only and do not
necessarily reflect those of the European Union or the European Research Council.
Neither the European Union nor the granting authority can be held responsible for
them.\r\nChristoph U. Günther and Krzysztof Pietrzak: This research was funded in
whole or in part by the Austrian Science Fund (FWF) 10.55776/F85. For open access
purposes, the author has applied a CC BY public copyright license to any author-accepted
manuscript version arising from this submission."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jesko
full_name: Dujmovic, Jesko
last_name: Dujmovic
- first_name: Christoph Ullrich
full_name: Günther, Christoph Ullrich
id: ec98511c-eb8e-11eb-b029-edd25d7271a1
last_name: Günther
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
citation:
ama: 'Dujmovic J, Günther CU, Pietrzak KZ. Space-deniable proofs. In: 23rd International
Conference on Theory of Cryptography. Vol 16271. Springer Nature; 2025:171-202.
doi:10.1007/978-3-032-12290-2_6'
apa: 'Dujmovic, J., Günther, C. U., & Pietrzak, K. Z. (2025). Space-deniable
proofs. In 23rd International Conference on Theory of Cryptography (Vol.
16271, pp. 171–202). Aarhus, Denmark: Springer Nature. https://doi.org/10.1007/978-3-032-12290-2_6'
chicago: Dujmovic, Jesko, Christoph Ullrich Günther, and Krzysztof Z Pietrzak. “Space-Deniable
Proofs.” In 23rd International Conference on Theory of Cryptography, 16271:171–202.
Springer Nature, 2025. https://doi.org/10.1007/978-3-032-12290-2_6.
ieee: J. Dujmovic, C. U. Günther, and K. Z. Pietrzak, “Space-deniable proofs,” in
23rd International Conference on Theory of Cryptography, Aarhus, Denmark,
2025, vol. 16271, pp. 171–202.
ista: 'Dujmovic J, Günther CU, Pietrzak KZ. 2025. Space-deniable proofs. 23rd International
Conference on Theory of Cryptography. TCC: Theory of Cryptography, LNCS, vol.
16271, 171–202.'
mla: Dujmovic, Jesko, et al. “Space-Deniable Proofs.” 23rd International Conference
on Theory of Cryptography, vol. 16271, Springer Nature, 2025, pp. 171–202,
doi:10.1007/978-3-032-12290-2_6.
short: J. Dujmovic, C.U. Günther, K.Z. Pietrzak, in:, 23rd International Conference
on Theory of Cryptography, Springer Nature, 2025, pp. 171–202.
conference:
end_date: 2025-12-05
location: Aarhus, Denmark
name: 'TCC: Theory of Cryptography'
start_date: 2025-12-01
corr_author: '1'
date_created: 2025-12-21T23:01:33Z
date_published: 2025-12-05T00:00:00Z
date_updated: 2025-12-29T11:44:16Z
day: '05'
department:
- _id: KrPi
doi: 10.1007/978-3-032-12290-2_6
intvolume: ' 16271'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2025/1723
month: '12'
oa: 1
oa_version: Preprint
page: 171-202
project:
- _id: 34a34d57-11ca-11ed-8bc3-a2688a8724e1
grant_number: F8509
name: Security and Privacy by Design for Complex Systems
publication: 23rd International Conference on Theory of Cryptography
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032122896'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Space-deniable proofs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16271
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20845'
abstract:
- lang: eng
text: "We develop new attacks against the Evasive LWE family of assumptions, in
both the public and private-coin regime. To the best of our knowledge, ours are
the first attacks against Evasive LWE in the public-coin regime, for any instantiation
from the family. Our attacks are summarized below.\r\n\r\nPublic-Coin Attacks.\r\n1.The
recent work by Hseih, Lin and Luo [17] constructed the first Attribute Based Encryption
(ABE) for unbounded depth circuits by relying on the “circular” evasive LWE assumption.
This assumption has been popularly considered as a safe, public-coin instance
of Evasive LWE in contrast to its “private-coin” cousins (for instance, see [10,
11]).\r\nWe provide the first attack against this assumption, challenging the
widely held belief that this is a public-coin assumption.\r\n2. We demonstrate
a counter-example against vanilla public-coin evasive LWE by Wee [26] in an unnatural
parameter regime. Our attack crucially relies on the error in the pre-condition
being larger than the error in the post-condition, necessitating a refinement
of the assumption.\r\n\r\nPrivate-Coin Attacks.\r\n1. The recent work by Agrawal,
Kumari and Yamada [2] constructed the first functional encryption scheme for pseudorandom
functionalities (PRFE) and extended this to obfuscation for pseudorandom functionalities
(PRIO) [4] by relying on private-coin evasive LWE. We provide a new attack against
the assumption stated in the first posting of their work (subsequently refined
to avoid these attacks).\r\n2. The recent work by Branco et al. [8] (concurrently
to [4]) provides a construction of obfuscation for pseudorandom functionalities
by relying on private-coin evasive LWE. We provide a new attack against their
stated assumption.\r\n3. Branco et al. [8] showed that there exist contrived,
“self-referential” classes of pseudorandom functionalities for which pseudorandom
obfuscation cannot exist. We extend their techniques to develop an analogous result
for pseudorandom functional encryption.\r\n\r\nWhile Evasive LWE was developed
to specifically avoid “zeroizing attacks”, our work shows that in certain settings,
such attacks can still apply."
acknowledgement: "We thank Rachel Lin for expressing concern about the applicability
of “HJL-style” attacks [15] on the construction in [2] during a talk by the first
author about [2]. This was the starting point of the investigation that led us to
develop the attack in [5, Sec 4.1]. The first author also thanks Hoeteck Wee for
sharing his rationale for introducing evasive LWE.\r\nThe first author is supported
by the CyStar center of excellence, the VHAR faculty chair, and the C3iHub fellowship.
The third author thanks Cystar, IIT Madras, for supporting a visit to IIT Madras
during which the collaboration was initiated. The 4th author is partly supported
by JST CREST Grant Number JPMJCR22M1."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Shweta
full_name: Agrawal, Shweta
last_name: Agrawal
- first_name: Anuja
full_name: Modi, Anuja
last_name: Modi
- first_name: Anshu
full_name: Yadav, Anshu
id: dc8f1524-403e-11ee-bf07-9649ad996e21
last_name: Yadav
- first_name: Shota
full_name: Yamada, Shota
last_name: Yamada
citation:
ama: 'Agrawal S, Modi A, Yadav A, Yamada S. Zeroizing attacks against evasive and circular
evasive LWE. In: 23rd International Conference on Theory of Cryptography.
Vol 16269. Springer Nature; 2025:259-290. doi:10.1007/978-3-032-12293-3_9'
apa: 'Agrawal, S., Modi, A., Yadav, A., & Yamada, S. (2025). Zeroizing attacks
against evasive and circular evasive LWE. In 23rd International Conference
on Theory of Cryptography (Vol. 16269, pp. 259–290). Aarhus, Denmark: Springer
Nature. https://doi.org/10.1007/978-3-032-12293-3_9'
chicago: Agrawal, Shweta, Anuja Modi, Anshu Yadav, and Shota Yamada. “Zeroizing
Attacks against Evasive and Circular Evasive LWE.” In 23rd International Conference
on Theory of Cryptography, 16269:259–90. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-12293-3_9.
ieee: S. Agrawal, A. Modi, A. Yadav, and S. Yamada, “Zeroizing attacks against evasive
and circular evasive LWE,” in 23rd International Conference on Theory of Cryptography,
Aarhus, Denmark, 2025, vol. 16269, pp. 259–290.
ista: 'Agrawal S, Modi A, Yadav A, Yamada S. 2025. Zeroizing attacks against evasive
and circular evasive LWE. 23rd International Conference on Theory of Cryptography.
TCC: Theory of Cryptography, LNCS, vol. 16269, 259–290.'
mla: Agrawal, Shweta, et al. “Zeroizing Attacks against Evasive and Circular Evasive
LWE.” 23rd International Conference on Theory of Cryptography, vol. 16269,
Springer Nature, 2025, pp. 259–90, doi:10.1007/978-3-032-12293-3_9.
short: S. Agrawal, A. Modi, A. Yadav, S. Yamada, in:, 23rd International Conference
on Theory of Cryptography, Springer Nature, 2025, pp. 259–290.
conference:
end_date: 2025-12-05
location: Aarhus, Denmark
name: 'TCC: Theory of Cryptography'
start_date: 2025-12-01
date_created: 2025-12-21T23:01:33Z
date_published: 2025-12-05T00:00:00Z
date_updated: 2025-12-29T11:51:13Z
day: '05'
department:
- _id: KrPi
doi: 10.1007/978-3-032-12293-3_9
intvolume: ' 16269'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2025/375
month: '12'
oa: 1
oa_version: Preprint
page: 259-290
publication: 23rd International Conference on Theory of Cryptography
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032122926'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Zeroizing attacks against evasive and circular evasive LWE
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16269
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20846'
abstract:
- lang: eng
text: "CVRFs are PRFs that unify the properties of verifiable and constrained PRFs.
Since they were introduced concurrently by Fuchsbauer and Chandran-Raghuraman-Vinayagamurthy
in 2014, it has been an open problem to construct CVRFs without using heavy machinery
such as multilinear maps, obfuscation or functional encryption.\r\nWe solve this
problem by constructing a prefix-constrained verifiable PRF that does not rely
on the aforementioned assumptions. Essentially, our construction is a verifiable
version of the Goldreich-Goldwasser-Micali PRF. To achieve verifiability we leverage
degree-2 algebraic PRGs and bilinear groups. In short, proofs consist of intermediate
values of the Goldreich-Goldwasser-Micali PRF raised to the exponents of group
elements. These outputs can be verified using pairings since the underlying PRG
is of degree 2.\r\nWe prove the selective security of our construction under the
Decisional Square Diffie-Hellman (DSDH) assumption and a new assumption, which
we dub recursive Decisional Diffie-Hellman (recursive DDH).\r\nWe prove the soundness
of recursive DDH in the generic group model assuming the hardness of the Multivariate
Quadratic (MQ) problem and a new variant thereof, which we call MQ+.\r\nLast,
in terms of applications, we observe that our CVRF is also an exponent (C)VRF
in the plain model. Exponent VRFs were recently introduced by Boneh et al. (Eurocrypt’25)
with various applications to threshold cryptography in mind. In addition to that,
we give further applications for prefix-CVRFs in the blockchain setting, namely,
stake-pooling and compressible randomness beacons."
acknowledgement: "We thank Jonas Steinbach and Gertjan De Mulder for helpful discussions
on BIP 32, Dennis Hofheinz and Julia Kastner for helpful discussions on early prototypes
of our CVRF, and Klaus Kraßnitzer for running pairing benchmarks on his MacBook
Pro.\r\nChristoph U. Günther: This research was funded in whole or in part by the
Austrian Science Fund (FWF) 10.55776/F85. For open access purposes, the author has
applied a CC BY public copyright license to any author-accepted manuscript version
arising from this submission."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Nicholas
full_name: Brandt, Nicholas
last_name: Brandt
- first_name: Miguel
full_name: Cueto Noval, Miguel
id: ffc563a3-f6e0-11ea-865d-e3cce03d17cc
last_name: Cueto Noval
orcid: 0000-0002-2505-4246
- first_name: Christoph Ullrich
full_name: Günther, Christoph Ullrich
id: ec98511c-eb8e-11eb-b029-edd25d7271a1
last_name: Günther
- first_name: Akin
full_name: Ünal, Akin
id: f6b56fb6-dc63-11ee-9dbf-f6780863a85a
last_name: Ünal
orcid: 0000-0002-8929-0221
- first_name: Stella
full_name: Wohnig, Stella
last_name: Wohnig
citation:
ama: 'Brandt N, Cueto Noval M, Günther CU, Ünal A, Wohnig S. Constrained verifiable
random functions without obfuscation and friends. In: 23rd International Conference
on Theory of Cryptography. Vol 16271. Springer Nature; 2025:478-511. doi:10.1007/978-3-032-12290-2_16'
apa: 'Brandt, N., Cueto Noval, M., Günther, C. U., Ünal, A., & Wohnig, S. (2025).
Constrained verifiable random functions without obfuscation and friends. In 23rd
International Conference on Theory of Cryptography (Vol. 16271, pp. 478–511).
Aarhus, Denmark: Springer Nature. https://doi.org/10.1007/978-3-032-12290-2_16'
chicago: Brandt, Nicholas, Miguel Cueto Noval, Christoph Ullrich Günther, Akin Ünal,
and Stella Wohnig. “Constrained Verifiable Random Functions without Obfuscation
and Friends.” In 23rd International Conference on Theory of Cryptography,
16271:478–511. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-12290-2_16.
ieee: N. Brandt, M. Cueto Noval, C. U. Günther, A. Ünal, and S. Wohnig, “Constrained
verifiable random functions without obfuscation and friends,” in 23rd International
Conference on Theory of Cryptography, Aarhus, Denmark, 2025, vol. 16271, pp.
478–511.
ista: 'Brandt N, Cueto Noval M, Günther CU, Ünal A, Wohnig S. 2025. Constrained
verifiable random functions without obfuscation and friends. 23rd International
Conference on Theory of Cryptography. TCC: Theory of Cryptography, LNCS, vol.
16271, 478–511.'
mla: Brandt, Nicholas, et al. “Constrained Verifiable Random Functions without Obfuscation
and Friends.” 23rd International Conference on Theory of Cryptography,
vol. 16271, Springer Nature, 2025, pp. 478–511, doi:10.1007/978-3-032-12290-2_16.
short: N. Brandt, M. Cueto Noval, C.U. Günther, A. Ünal, S. Wohnig, in:, 23rd International
Conference on Theory of Cryptography, Springer Nature, 2025, pp. 478–511.
conference:
end_date: 2025-12-05
location: Aarhus, Denmark
name: 'TCC: Theory of Cryptography'
start_date: 2025-12-01
corr_author: '1'
date_created: 2025-12-21T23:01:34Z
date_published: 2025-12-05T00:00:00Z
date_updated: 2025-12-29T11:11:29Z
day: '05'
department:
- _id: KrPi
doi: 10.1007/978-3-032-12290-2_16
intvolume: ' 16271'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2025/1045
month: '12'
oa: 1
oa_version: Preprint
page: 478-511
project:
- _id: 34a34d57-11ca-11ed-8bc3-a2688a8724e1
grant_number: F8509
name: Security and Privacy by Design for Complex Systems
publication: 23rd International Conference on Theory of Cryptography
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032122896'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Constrained verifiable random functions without obfuscation and friends
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16271
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_place: repository
OA_type: green
_id: '21262'
abstract:
- lang: eng
text: "Continuous Group Key Agreement (CGKA) is the primitive underlying secure
group messaging. It allows a large group of N users to maintain a shared secret
key that is frequently rotated by the\r\ngroup members in order to achieve forward
secrecy and post compromise security. The group messaging scheme Messaging Layer
Security (MLS) standardized by the IETF makes use of a CGKA called TreeKEM which
arranges the N group members in a binary tree. Here, each node is associated with
a public-key, each user is assigned one of the leaves, and a user knows the corresponding
secret keys from their leaf to the root. To update the key material known to them,
a user must just replace keys at log(N) nodes, which requires them to create and
upload log(N) ciphertexts. Such updates must be processed sequentially by all
users, which for large groups is impractical. To allow for concurrent updates,
TreeKEM uses the “propose and commit” paradigm, where multiple users can concurrently
propose to update (by just sampling a fresh leaf key), and a single user can then
commit to all proposals at once. Unfortunately, this process destroys the binary
tree structure as the tree gets pruned and some nodes must be “blanked” at the
cost of increasing the in-degree of others, which makes the commit operation,
as well as, future commits more costly. In the worst case, the update cost (in
terms of uploaded ciphertexts) per user can grow from log(N) to Ω(N). In this
work we provide two main contributions. First, we show that MLS’ communication
complexity is bad not only in the worst case but also if the proposers and committers
are chosen at random: even if there’s just one update proposal for every commit
the expected cost is already over √N, and it approaches N as this ratio changes
towards more proposals. Our second contribution is a new variant of propose and
commit for\r\nTreeKEM which for moderate amounts of update proposals per commit
provably achieves an update cost of Θ(log(N)) assuming the proposers and committers
are chosen at random."
acknowledgement: B. Auerbach and B. Erol—Conducted part of this work at ISTA.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Benedikt
full_name: Auerbach, Benedikt
id: D33D2B18-E445-11E9-ABB7-15F4E5697425
last_name: Auerbach
orcid: 0000-0002-7553-6606
- first_name: Miguel
full_name: Cueto Noval, Miguel
id: ffc563a3-f6e0-11ea-865d-e3cce03d17cc
last_name: Cueto Noval
orcid: 0000-0002-2505-4246
- first_name: Boran
full_name: Erol, Boran
last_name: Erol
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
citation:
ama: 'Auerbach B, Cueto Noval M, Erol B, Pietrzak KZ. Continuous group-key agreement:
Concurrent updates without pruning. In: 45th Annual International Cryptology
Conference. Vol 16007. Springer Nature; 2025:141-172. doi:10.1007/978-3-032-01913-4_5'
apa: 'Auerbach, B., Cueto Noval, M., Erol, B., & Pietrzak, K. Z. (2025). Continuous
group-key agreement: Concurrent updates without pruning. In 45th Annual International
Cryptology Conference (Vol. 16007, pp. 141–172). Santa Barbara, CA, United
States: Springer Nature. https://doi.org/10.1007/978-3-032-01913-4_5'
chicago: 'Auerbach, Benedikt, Miguel Cueto Noval, Boran Erol, and Krzysztof Z Pietrzak.
“Continuous Group-Key Agreement: Concurrent Updates without Pruning.” In 45th
Annual International Cryptology Conference, 16007:141–72. Springer Nature,
2025. https://doi.org/10.1007/978-3-032-01913-4_5.'
ieee: 'B. Auerbach, M. Cueto Noval, B. Erol, and K. Z. Pietrzak, “Continuous group-key
agreement: Concurrent updates without pruning,” in 45th Annual International
Cryptology Conference, Santa Barbara, CA, United States, 2025, vol. 16007,
pp. 141–172.'
ista: 'Auerbach B, Cueto Noval M, Erol B, Pietrzak KZ. 2025. Continuous group-key
agreement: Concurrent updates without pruning. 45th Annual International Cryptology
Conference. CRYPTO: International Cryptology Conference, LNCS, vol. 16007, 141–172.'
mla: 'Auerbach, Benedikt, et al. “Continuous Group-Key Agreement: Concurrent Updates
without Pruning.” 45th Annual International Cryptology Conference, vol.
16007, Springer Nature, 2025, pp. 141–72, doi:10.1007/978-3-032-01913-4_5.'
short: B. Auerbach, M. Cueto Noval, B. Erol, K.Z. Pietrzak, in:, 45th Annual International
Cryptology Conference, Springer Nature, 2025, pp. 141–172.
conference:
end_date: 2025-08-21
location: Santa Barbara, CA, United States
name: 'CRYPTO: International Cryptology Conference'
start_date: 2025-08-17
date_created: 2026-02-17T07:41:04Z
date_published: 2025-08-17T00:00:00Z
date_updated: 2026-02-18T07:36:42Z
day: '17'
department:
- _id: KrPi
doi: 10.1007/978-3-032-01913-4_5
intvolume: ' 16007'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2025/1035
month: '08'
oa: 1
oa_version: Preprint
page: 141-172
publication: 45th Annual International Cryptology Conference
publication_identifier:
eisbn:
- '9783032019134'
eissn:
- 1611-3349
isbn:
- '9783032019127'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: 'Continuous group-key agreement: Concurrent updates without pruning'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16007
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '21323'
abstract:
- lang: eng
text: We present a unifying framework for proving the knowledge-soundness of KZG-like
polynomial commitment schemes, encompassing both univariate and multivariate variants.
By conceptualizing the proof technique of Lipmaa, Parisella, and Siim for the
univariate KZG scheme (EUROCRYPT 2024), we present tools and falsifiable hardness
assumptions that permit black-box extraction of the multivariate KZG scheme. Central
to our approach is the notion of a canonical Proof-of-Knowledge of a Polynomial
(PoKoP) of a polynomial commitment scheme, which we use to capture the extractability
notion required in constructions of practical zk-SNARKs. We further present an
explicit polynomial decomposition lemma for multivariate polynomials, enabling
a more direct analysis of interpolating extractors and bridging the gap between
univariate and multivariate commitments. Our results provide the first standard-model
proofs of extractability for the multivariate KZG scheme and many of its variants
under falsifiable assumptions.
acknowledgement: Juraj Belohorec, Pavel Hubáček, and Kristýna Mašková were partially
supported by the Academy of Sciences of the Czech Republic (RVO 67985840), Czech
Science Foundation GAČR grant No. 25-16311S, and by Zircuit. Pavel Dvořák was supported
by Czech Science Foundation GAČR grant No. 22-14872O. Juraj Belohorec and Kristýna
Mašková were supported by the grant SVV–2025–260822.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Juraj
full_name: Belohorec, Juraj
last_name: Belohorec
- first_name: Pavel
full_name: Dvořák, Pavel
last_name: Dvořák
- first_name: Charlotte
full_name: Hoffmann, Charlotte
id: 0f78d746-dc7d-11ea-9b2f-83f92091afe7
last_name: Hoffmann
orcid: 0000-0003-2027-5549
- first_name: Pavel
full_name: Hubáček, Pavel
last_name: Hubáček
- first_name: Kristýna
full_name: Mašková, Kristýna
last_name: Mašková
- first_name: Martin
full_name: Pastyřík, Martin
last_name: Pastyřík
citation:
ama: 'Belohorec J, Dvořák P, Hoffmann C, Hubáček P, Mašková K, Pastyřík M. On extractability
of the KZG family of polynomial commitment schemes. In: 45th Annual International
Cryptology Conference. Vol 16005. Springer Nature; 2025:584-616. doi:10.1007/978-3-032-01887-8_19'
apa: 'Belohorec, J., Dvořák, P., Hoffmann, C., Hubáček, P., Mašková, K., & Pastyřík,
M. (2025). On extractability of the KZG family of polynomial commitment schemes.
In 45th Annual International Cryptology Conference (Vol. 16005, pp. 584–616).
Santa Barbara, CA, United States: Springer Nature. https://doi.org/10.1007/978-3-032-01887-8_19'
chicago: Belohorec, Juraj, Pavel Dvořák, Charlotte Hoffmann, Pavel Hubáček, Kristýna
Mašková, and Martin Pastyřík. “On Extractability of the KZG Family of Polynomial
Commitment Schemes.” In 45th Annual International Cryptology Conference,
16005:584–616. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-01887-8_19.
ieee: J. Belohorec, P. Dvořák, C. Hoffmann, P. Hubáček, K. Mašková, and M. Pastyřík,
“On extractability of the KZG family of polynomial commitment schemes,” in 45th
Annual International Cryptology Conference, Santa Barbara, CA, United States,
2025, vol. 16005, pp. 584–616.
ista: 'Belohorec J, Dvořák P, Hoffmann C, Hubáček P, Mašková K, Pastyřík M. 2025.
On extractability of the KZG family of polynomial commitment schemes. 45th Annual
International Cryptology Conference. CRYPTO: International Cryptology Conference,
LNCS, vol. 16005, 584–616.'
mla: Belohorec, Juraj, et al. “On Extractability of the KZG Family of Polynomial
Commitment Schemes.” 45th Annual International Cryptology Conference, vol.
16005, Springer Nature, 2025, pp. 584–616, doi:10.1007/978-3-032-01887-8_19.
short: J. Belohorec, P. Dvořák, C. Hoffmann, P. Hubáček, K. Mašková, M. Pastyřík,
in:, 45th Annual International Cryptology Conference, Springer Nature, 2025, pp.
584–616.
conference:
end_date: 2025-08-221
location: Santa Barbara, CA, United States
name: 'CRYPTO: International Cryptology Conference'
start_date: 2025-08-17
date_created: 2026-02-18T10:59:58Z
date_published: 2025-08-17T00:00:00Z
date_updated: 2026-02-19T07:50:33Z
day: '17'
department:
- _id: KrPi
doi: 10.1007/978-3-032-01887-8_19
intvolume: ' 16005'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2025/514
month: '08'
oa: 1
oa_version: Preprint
page: 584-616
publication: 45th Annual International Cryptology Conference
publication_identifier:
eisbn:
- '9783032018878'
eissn:
- 1611-3349
isbn:
- '9783032018861'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: On extractability of the KZG family of polynomial commitment schemes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16005
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19741'
abstract:
- lang: eng
text: 'Quantitative automata model beyond-boolean aspects of systems: every execution
is mapped to a real number by incorporating weighted transitions and value functions
that generalize acceptance conditions of boolean w-automata. Despite the theoretical
advances in systems analysis through quantitative automata, the first comprehensive
software tool for quantitative automata (Quantitative Automata Kit, or QuAK) was
developed only recently. QuAK implements algorithms for solving standard decision
problems, e.g., emptiness and universality, as well as constructions for safety
and liveness of quantitative automata. We present the architecture of QuAK, which
reflects that all of these problems reduce to either checking inclusion between
two quantitative automata or computing the highest value achievable by an automaton—its
so-called top value. We improve QuAK by extending these two algorithms with an
option to return, alongside their results, an ultimately periodic word witnessing
the algorithm’s output, as well as implementing a new safety-liveness decomposition
algorithm that can handle nondeterministic automata, making QuAK more informative
and capable.'
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093.
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: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. Automating the analysis of
quantitative automata with QuAK. In: 31st International Conference on Tools
and Algorithms for the Construction and Analysis of Systems. Vol 15696. Springer
Nature; 2025:303-312. doi:10.1007/978-3-031-90643-5_16'
apa: Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2025).
Automating the analysis of quantitative automata with QuAK. In 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 15696, pp. 303–312). Springer Nature. https://doi.org/10.1007/978-3-031-90643-5_16
chicago: Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci
E Sarac. “Automating the Analysis of Quantitative Automata with QuAK.” In 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, 15696:303–12. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-90643-5_16.
ieee: M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Automating
the analysis of quantitative automata with QuAK,” in 31st International Conference
on Tools and Algorithms for the Construction and Analysis of Systems, 2025,
vol. 15696, pp. 303–312.
ista: Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2025. Automating the analysis
of quantitative automata with QuAK. 31st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 15696, 303–312.
mla: Chalupa, Marek, et al. “Automating the Analysis of Quantitative Automata with
QuAK.” 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 15696, Springer Nature, 2025, pp. 303–12, doi:10.1007/978-3-031-90643-5_16.
short: M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Springer Nature, 2025, pp. 303–312.
corr_author: '1'
date_created: 2025-05-25T22:17:07Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-90643-5_16
ec_funded: 1
external_id:
arxiv:
- '2501.16088'
file:
- access_level: open_access
checksum: a27fa245be8d83421e9127b48a09c8af
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T08:13:11Z
date_updated: 2025-06-02T08:13:11Z
file_id: '19768'
file_name: 2025_TACAS_ChalupaMarek.pdf
file_size: 420669
relation: main_file
success: 1
file_date_updated: 2025-06-02T08:13:11Z
has_accepted_license: '1'
intvolume: ' 15696'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 303-312
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906428'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '20147'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Automating the analysis of quantitative automata with QuAK
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: 15696
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19778'
abstract:
- lang: eng
text: "A verifiable delay function VDF(x, T)->(y, π) maps an input x and time parameter
T to an output y together with an efficiently verifiable proof π certifying that
y was correctly computed. The function runs in T sequential steps, and it should
not be possible to compute y much faster than that. The only known practical VDFs
use sequential squaring in groups of unknown order as the sequential function,
i.e., y = x^2^T. There are two constructions for the proof of exponentiation (PoE)
certifying that y = x^2^T, with Wesolowski (Eurocrypt’19) having very short proofs,
but they are more expensive to compute and the soundness relies on stronger assumptions
than the PoE proposed by Pietrzak (ITCS’19).\r\nA recent application of VDFs by
Arun, Bonneau and Clark (Asiacrypt’22) are short-lived proofs and signatures,
which are proofs and signatures that are only sound for some time t, but after
that can be forged by anyone. For this they rely on “watermarkable VDFs”, where
the proof embeds a prover chosen watermark. To achieve stronger notions of proofs/signatures
with reusable forgeability, they rely on “zero-knowledge VDFs”, where instead
of the output y, one just proves knowledge of this output. The existing proposals
for watermarkable and zero-knowledge VDFs all build on Wesolowski’s PoE, for the
watermarkable VDFs there’s currently no security proof.\r\n\r\nIn this work we
give the first constructions that transform any PoEs in hidden order groups into
watermarkable VDFs and into zkVDFs, solving an open question by Arun et al. Unlike
our watermarkable VDF, the zkVDF (required for reusable forgeability) is not very
practical as the number of group elements in the proof is a security parameter.
To address this, we introduce the notion of zero-knowledge proofs of sequential
work (zkPoSW), a notion that relaxes zkVDFs by not requiring that the output is
unique. We show that zkPoSW are sufficient to construct proofs or signatures with
reusable forgeability, and construct efficient zkPoSW from any PoE, ultimately
achieving short lived proofs and signatures that improve upon Arun et al.’s construction
in several dimensions (faster forging times, arguably weaker assumptions).\r\nA
key idea underlying our constructions is to not directly construct a (watermarked
or zk) proof for y = x^2^T, but instead give a (watermarked or zk) proof for the
more basic statement that \r\nx^l, y^l satisfy x^l = x ^r, y^l = y^r for some
r, together with a normal PoE for y^l = (x^l)^2^T."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Charlotte
full_name: Hoffmann, Charlotte
id: 0f78d746-dc7d-11ea-9b2f-83f92091afe7
last_name: Hoffmann
orcid: 0000-0003-2027-5549
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
citation:
ama: 'Hoffmann C, Pietrzak KZ. Watermarkable and zero-knowledge Verifiable Delay
Functions from any proof of exponentiation. In: 28th IACR International Conference
on Practice and Theory of Public-Key Cryptography. Vol 15674. Springer Nature;
2025:36-66. doi:10.1007/978-3-031-91820-9_2'
apa: 'Hoffmann, C., & Pietrzak, K. Z. (2025). Watermarkable and zero-knowledge
Verifiable Delay Functions from any proof of exponentiation. In 28th IACR International
Conference on Practice and Theory of Public-Key Cryptography (Vol. 15674,
pp. 36–66). Roros, Norway: Springer Nature. https://doi.org/10.1007/978-3-031-91820-9_2'
chicago: Hoffmann, Charlotte, and Krzysztof Z Pietrzak. “Watermarkable and Zero-Knowledge
Verifiable Delay Functions from Any Proof of Exponentiation.” In 28th IACR
International Conference on Practice and Theory of Public-Key Cryptography,
15674:36–66. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-91820-9_2.
ieee: C. Hoffmann and K. Z. Pietrzak, “Watermarkable and zero-knowledge Verifiable
Delay Functions from any proof of exponentiation,” in 28th IACR International
Conference on Practice and Theory of Public-Key Cryptography, Roros, Norway,
2025, vol. 15674, pp. 36–66.
ista: 'Hoffmann C, Pietrzak KZ. 2025. Watermarkable and zero-knowledge Verifiable
Delay Functions from any proof of exponentiation. 28th IACR International Conference
on Practice and Theory of Public-Key Cryptography. PKC: Public-Key Cryptography,
LNCS, vol. 15674, 36–66.'
mla: Hoffmann, Charlotte, and Krzysztof Z. Pietrzak. “Watermarkable and Zero-Knowledge
Verifiable Delay Functions from Any Proof of Exponentiation.” 28th IACR International
Conference on Practice and Theory of Public-Key Cryptography, vol. 15674,
Springer Nature, 2025, pp. 36–66, doi:10.1007/978-3-031-91820-9_2.
short: C. Hoffmann, K.Z. Pietrzak, in:, 28th IACR International Conference on Practice
and Theory of Public-Key Cryptography, Springer Nature, 2025, pp. 36–66.
conference:
end_date: 2025-05-15
location: Roros, Norway
name: 'PKC: Public-Key Cryptography'
start_date: 2025-05-12
corr_author: '1'
date_created: 2025-06-03T07:30:21Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2026-04-16T09:11:09Z
day: '01'
department:
- _id: KrPi
- _id: GradSch
doi: 10.1007/978-3-031-91820-9_2
intvolume: ' 15674'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://ia.cr/2024/481
month: '01'
oa: 1
oa_version: Preprint
page: 36-66
publication: 28th IACR International Conference on Practice and Theory of Public-Key
Cryptography
publication_identifier:
eisbn:
- '9783031918209'
eissn:
- 1611-3349
isbn:
- '9783031918193'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '20920'
relation: dissertation_contains
status: public
- id: '20556'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Watermarkable and zero-knowledge Verifiable Delay Functions from any proof
of exponentiation
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 15674
year: '2025'
...
---
_id: '18155'
abstract:
- lang: eng
text: We study the classical problem of verifying programs with respect to formal
specifications given in the linear temporal logic (LTL). We first present novel
sound and complete witnesses for LTL verification over imperative programs. Our
witnesses are applicable to both verification (proving) and refutation (finding
bugs) settings. We then consider LTL formulas in which atomic propositions can
be polynomial constraints and turn our focus to polynomial arithmetic programs,
i.e. programs in which every assignment and guard consists only of polynomial
expressions. For this setting, we provide an efficient algorithm to automatically
synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete.
Finally, we present experimental results demonstrating the effectiveness of our
approach and that it can handle programs which were beyond the reach of previous
state-of-the-art tools.
acknowledgement: This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt)
and the Hong Kong Research Grants Council ECS Project Number 26208122.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Ehsan
full_name: Goharshady, Ehsan
last_name: Goharshady
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. Sound and complete
witnesses for template-based verification of LTL properties on polynomial programs.
In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in
Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 14933. Springer
Nature; 2024:600-619. doi:10.1007/978-3-031-71162-6_31'
apa: 'Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., & Zikelic,
D. (2024). Sound and complete witnesses for template-based verification of LTL
properties on polynomial programs. In Lecture Notes in Computer Science (including
subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
(Vol. 14933, pp. 600–619). Milan, Italy: Springer Nature. https://doi.org/10.1007/978-3-031-71162-6_31'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad
Karrabi, and Dorde Zikelic. “Sound and Complete Witnesses for Template-Based Verification
of LTL Properties on Polynomial Programs.” In Lecture Notes in Computer Science
(Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), 14933:600–619. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-71162-6_31.
ieee: K. Chatterjee, A. K. Goharshady, E. Goharshady, M. Karrabi, and D. Zikelic,
“Sound and complete witnesses for template-based verification of LTL properties
on polynomial programs,” in Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
Milan, Italy, 2024, vol. 14933, pp. 600–619.
ista: 'Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. 2024. Sound
and complete witnesses for template-based verification of LTL properties on polynomial
programs. Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics). FM: Formal Methods,
LNCS, vol. 14933, 600–619.'
mla: Chatterjee, Krishnendu, et al. “Sound and Complete Witnesses for Template-Based
Verification of LTL Properties on Polynomial Programs.” Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics), vol. 14933, Springer Nature, 2024, pp. 600–19, doi:10.1007/978-3-031-71162-6_31.
short: K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, D. Zikelic, in:,
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp.
600–619.
conference:
end_date: 2024-09-13
location: Milan, Italy
name: 'FM: Formal Methods'
start_date: 2024-09-09
corr_author: '1'
date_created: 2024-09-29T22:01:37Z
date_published: 2024-09-11T00:00:00Z
date_updated: 2025-09-08T09:51:34Z
day: '11'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-71162-6_31
ec_funded: 1
external_id:
arxiv:
- '2403.05386'
isi:
- '001336893300031'
file:
- access_level: open_access
checksum: 223845be9e754681ee218866827c95e7
content_type: application/pdf
creator: dernst
date_created: 2024-10-01T09:56:54Z
date_updated: 2024-10-01T09:56:54Z
file_id: '18165'
file_name: 2024_LNCS_Chatterjee.pdf
file_size: 650495
relation: main_file
success: 1
file_date_updated: 2024-10-01T09:56:54Z
has_accepted_license: '1'
intvolume: ' 14933'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 600-619
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031711619'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Sound and complete witnesses for template-based verification of LTL properties
on polynomial programs
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14933
year: '2024'
...
---
_id: '18177'
abstract:
- lang: eng
text: Partially Specified Boolean Networks (PSBNs) represent a family of Boolean
models resulting from possible interpretations of unknown update logics. Hybrid
extension of CTL (HCTL) has the power to express complex dynamical phenomena,
such as oscillations or stability. We present BNClassifier to classify Boolean
Networks corresponding to a given PSBN according to criteria specified in HCTL.
The implementation of the tool is fully symbolic (based on BDDs). The results
are visualised using the machine-learning-based technology of decision trees.
acknowledgement: The work has been supported by the Czech Science Foundation grant
No. GA22-10845S. This project has received funding from the European Union’s Horizon
2020 research and innovation programme under the Marie Sklodowska-Curie Grant Agreement
No. 101034413.
alternative_title:
- LNBI
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Luboš
full_name: Brim, Luboš
last_name: Brim
- first_name: Ondřej
full_name: Huvar, Ondřej
last_name: Huvar
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: David
full_name: Šafránek, David
last_name: Šafránek
citation:
ama: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. BNClassifier: Classifying
boolean models by dynamic properties. In: Computational Methods in Systems
Biology. Vol 14971. Springer Nature; 2024:19-26. doi:10.1007/978-3-031-71671-3_2'
apa: 'Beneš, N., Brim, L., Huvar, O., Pastva, S., & Šafránek, D. (2024). BNClassifier:
Classifying boolean models by dynamic properties. In Computational Methods
in Systems Biology (Vol. 14971, pp. 19–26). Springer Nature. https://doi.org/10.1007/978-3-031-71671-3_2'
chicago: 'Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek.
“BNClassifier: Classifying Boolean Models by Dynamic Properties.” In Computational
Methods in Systems Biology, 14971:19–26. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-71671-3_2.'
ieee: 'N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “BNClassifier: Classifying
boolean models by dynamic properties,” in Computational Methods in Systems
Biology, 2024, vol. 14971, pp. 19–26.'
ista: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. 2024. BNClassifier: Classifying
boolean models by dynamic properties. Computational Methods in Systems Biology.
, LNBI, vol. 14971, 19–26.'
mla: 'Beneš, Nikola, et al. “BNClassifier: Classifying Boolean Models by Dynamic
Properties.” Computational Methods in Systems Biology, vol. 14971, Springer
Nature, 2024, pp. 19–26, doi:10.1007/978-3-031-71671-3_2.'
short: N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, in:, Computational Methods
in Systems Biology, Springer Nature, 2024, pp. 19–26.
date_created: 2024-10-06T22:01:12Z
date_published: 2024-09-19T00:00:00Z
date_updated: 2025-09-08T09:54:27Z
day: '19'
department:
- _id: ToHe
doi: 10.1007/978-3-031-71671-3_2
ec_funded: 1
external_id:
isi:
- '001333144400002'
intvolume: ' 14971'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 19-26
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Computational Methods in Systems Biology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031716706'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'BNClassifier: Classifying boolean models by dynamic properties'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14971
year: '2024'
...
---
_id: '18206'
abstract:
- lang: eng
text: In the context of in vitro fertilization (IVF), selecting embryos for transfer
is critical in determining pregnancy outcomes, with implantation as the essential
first milestone for a successful pregnancy. This study introduces the Bonna algorithm,
an advanced deep-learning framework engineered to predict embryo implantation
probabilities. The algorithm employs a sophisticated integration of machine-learning
techniques, utilizing MobileNetV2 for pixel and context embedding, a custom Pix2Pix
model for precise segmentation, and a Vision Transformer for additional depth
in embedding. MobileNetV2 was chosen for its robust feature extraction capabilities,
focusing on textures and edges. The custom Pix2Pix model is adapted for precise
segmentation of significant biological features such as the zona pellucida and
blastocyst cavity. The Vision Transformer adds a global perspective, capturing
complex patterns not apparent in local image segments. Tested on a dataset of
images of human blastocysts collected from Ukraine, Israel, and Spain, the Bonna
algorithm was rigorously validated through 10-fold cross-validation to ensure
its robustness and reliability. It demonstrates superior performance with a mean
area under the receiver operating characteristic curve (AUC) of 0.754, significantly
outperforming existing models. The study not only advances predictive accuracy
in embryo selection but also highlights the algorithm’s clinical applicability
due to reliable confidence reporting.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Gilad
full_name: Rave, Gilad
last_name: Rave
- first_name: Daniel E.
full_name: Fordham, Daniel E.
last_name: Fordham
- first_name: Alexander
full_name: Bronstein, Alexander
id: 58f3726e-7cba-11ef-ad8b-e6e8cb3904e6
last_name: Bronstein
orcid: 0000-0001-9699-8730
- first_name: David H.
full_name: Silver, David H.
last_name: Silver
citation:
ama: 'Rave G, Fordham DE, Bronstein AM, Silver DH. Enhancing predictive accuracy
in embryo implantation: The Bonna algorithm and its clinical implications. In:
First International Conference on Artificial Intelligence in Healthcare.
Vol 14976. Springer Nature; 2024:160-171. doi:10.1007/978-3-031-67285-9_12'
apa: 'Rave, G., Fordham, D. E., Bronstein, A. M., & Silver, D. H. (2024). Enhancing
predictive accuracy in embryo implantation: The Bonna algorithm and its clinical
implications. In First International Conference on Artificial Intelligence
in Healthcare (Vol. 14976, pp. 160–171). Swansea, United Kingdom: Springer
Nature. https://doi.org/10.1007/978-3-031-67285-9_12'
chicago: 'Rave, Gilad, Daniel E. Fordham, Alex M. Bronstein, and David H. Silver.
“Enhancing Predictive Accuracy in Embryo Implantation: The Bonna Algorithm and Its
Clinical Implications.” In First International Conference on Artificial Intelligence
in Healthcare, 14976:160–71. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-67285-9_12.'
ieee: 'G. Rave, D. E. Fordham, A. M. Bronstein, and D. H. Silver, “Enhancing predictive
accuracy in embryo implantation: The Bonna algorithm and its clinical implications,”
in First International Conference on Artificial Intelligence in Healthcare,
Swansea, United Kingdom, 2024, vol. 14976, pp. 160–171.'
ista: 'Rave G, Fordham DE, Bronstein AM, Silver DH. 2024. Enhancing predictive accuracy
in embryo implantation: The Bonna algorithm and its clinical implications. First
International Conference on Artificial Intelligence in Healthcare. AIiH: Artificial
Intelligence in Healthcare, LNCS, vol. 14976, 160–171.'
mla: 'Rave, Gilad, et al. “Enhancing Predictive Accuracy in Embryo Implantation:
The Bonna Algorithm and Its Clinical Implications.” First International Conference
on Artificial Intelligence in Healthcare, vol. 14976, Springer Nature, 2024,
pp. 160–71, doi:10.1007/978-3-031-67285-9_12.'
short: G. Rave, D.E. Fordham, A.M. Bronstein, D.H. Silver, in:, First International
Conference on Artificial Intelligence in Healthcare, Springer Nature, 2024, pp.
160–171.
conference:
end_date: 2024-09-06
location: Swansea, United Kingdom
name: 'AIiH: Artificial Intelligence in Healthcare'
start_date: 2024-09-04
date_created: 2024-10-08T12:46:23Z
date_published: 2024-08-15T00:00:00Z
date_updated: 2024-10-09T10:33:39Z
day: '15'
doi: 10.1007/978-3-031-67285-9_12
extern: '1'
intvolume: ' 14976'
language:
- iso: eng
month: '08'
oa_version: None
page: 160-171
publication: First International Conference on Artificial Intelligence in Healthcare
publication_identifier:
eisbn:
- '9783031672859'
eissn:
- 1611-3349
isbn:
- '9783031672842'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Enhancing predictive accuracy in embryo implantation: The Bonna algorithm
and its clinical implications'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14976
year: '2024'
...
---
APC_amount: 2290 EUR
OA_place: publisher
OA_type: hybrid
_id: '18521'
abstract:
- lang: eng
text: In distributed systems with processes that do not share a global clock, partial
synchrony is achieved by clock synchronization that guarantees bounded clock skew
among all applications. Existing solutions for distributed runtime verification
under partial synchrony against temporal logic specifications are exact but suffer
from significant computational overhead. In this paper, we propose an approximate
distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates
this issue by abstracting away potential interleaving behaviors. This conservative
abstraction enables a significant speedup of the distributed monitors, albeit
with a tradeoff in accuracy. We address this tradeoff with a methodology that
combines our approximate monitor with its exact counterpart, resulting in enhanced
efficiency without sacrificing precision. We evaluate our approach with multiple
experiments, showcasing its efficacy in both real-world applications and synthetic
examples.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. This
work is sponsored in part by the United States NSF CCF-2118356 award. This research
was partially funded by A-IQ Ready (Chips JU, grant agreement No. 101096658).
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Borzoo
full_name: Bonakdarpour, Borzoo
last_name: Bonakdarpour
- first_name: Anik
full_name: Momtaz, Anik
last_name: Momtaz
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. Approximate distributed monitoring
under partial synchrony: Balancing speed & accuracy. In: 24th International
Conference on Runtime Verification. Vol 15191. Springer Nature; 2024:282-301.
doi:10.1007/978-3-031-74234-7_18'
apa: 'Bonakdarpour, B., Momtaz, A., Nickovic, D., & Sarac, N. E. (2024). Approximate
distributed monitoring under partial synchrony: Balancing speed & accuracy.
In 24th International Conference on Runtime Verification (Vol. 15191, pp.
282–301). Istanbul, Turkey: Springer Nature. https://doi.org/10.1007/978-3-031-74234-7_18'
chicago: 'Bonakdarpour, Borzoo, Anik Momtaz, Dejan Nickovic, and Naci E Sarac. “Approximate
Distributed Monitoring under Partial Synchrony: Balancing Speed & Accuracy.”
In 24th International Conference on Runtime Verification, 15191:282–301.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-74234-7_18.'
ieee: 'B. Bonakdarpour, A. Momtaz, D. Nickovic, and N. E. Sarac, “Approximate distributed
monitoring under partial synchrony: Balancing speed & accuracy,” in 24th
International Conference on Runtime Verification, Istanbul, Turkey, 2024,
vol. 15191, pp. 282–301.'
ista: 'Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. 2024. Approximate distributed
monitoring under partial synchrony: Balancing speed & accuracy. 24th International
Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS,
vol. 15191, 282–301.'
mla: 'Bonakdarpour, Borzoo, et al. “Approximate Distributed Monitoring under Partial
Synchrony: Balancing Speed & Accuracy.” 24th International Conference on
Runtime Verification, vol. 15191, Springer Nature, 2024, pp. 282–301, doi:10.1007/978-3-031-74234-7_18.'
short: B. Bonakdarpour, A. Momtaz, D. Nickovic, N.E. Sarac, in:, 24th International
Conference on Runtime Verification, Springer Nature, 2024, pp. 282–301.
conference:
end_date: 2024-10-17
location: Istanbul, Turkey
name: 'RV: Conference on Runtime Verification'
start_date: 2024-10-15
corr_author: '1'
date_created: 2024-11-10T23:01:58Z
date_published: 2024-10-12T00:00:00Z
date_updated: 2025-09-08T14:39:14Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
- _id: GradSch
doi: 10.1007/978-3-031-74234-7_18
ec_funded: 1
external_id:
arxiv:
- '2408.05033'
isi:
- '001420093700018'
file:
- access_level: open_access
checksum: 7b8ca21b8c19ab796fa445b0e54003ca
content_type: application/pdf
creator: dernst
date_created: 2024-11-11T09:42:28Z
date_updated: 2024-11-11T09:42:28Z
file_id: '18539'
file_name: 2024_LNCS_Bonakdarpour.pdf
file_size: 1897101
relation: main_file
success: 1
file_date_updated: 2024-11-11T09:42:28Z
has_accepted_license: '1'
intvolume: ' 15191'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 282-301
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 24th International Conference on Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031742330'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Approximate distributed monitoring under partial synchrony: Balancing speed
& accuracy'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15191
year: '2024'
...
---
OA_type: closed access
_id: '18563'
abstract:
- lang: eng
text: I give a personal account about the wave of new research activities that rose
in the 1990s on the specification, verification, and control of real-time systems.
acknowledgement: I thank all my collaborators over the years. None of the mentioned
contributions would have been possible without them. I also apologize for all omissions.
The selection of contributions in this essay reflects primarily my personal involvement
rather than any measure of importance.
alternative_title:
- LNCS
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. Reminiscences of a Real-Time Researcher. In: Graf S, Pettersson
P, Steffen B, eds. Real Time and Such. Vol 15230. LNCS. Cham: Springer
Nature; 2024:154-164. doi:10.1007/978-3-031-73751-0_12'
apa: 'Henzinger, T. A. (2024). Reminiscences of a Real-Time Researcher. In S. Graf,
P. Pettersson, & B. Steffen (Eds.), Real Time and Such (Vol. 15230,
pp. 154–164). Cham: Springer Nature. https://doi.org/10.1007/978-3-031-73751-0_12'
chicago: 'Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” In Real
Time and Such, edited by Susanne Graf, Paul Pettersson, and Bernhard Steffen,
15230:154–64. LNCS. Cham: Springer Nature, 2024. https://doi.org/10.1007/978-3-031-73751-0_12.'
ieee: 'T. A. Henzinger, “Reminiscences of a Real-Time Researcher,” in Real Time
and Such, vol. 15230, S. Graf, P. Pettersson, and B. Steffen, Eds. Cham: Springer
Nature, 2024, pp. 154–164.'
ista: 'Henzinger TA. 2024.Reminiscences of a Real-Time Researcher. In: Real Time
and Such. LNCS, vol. 15230, 154–164.'
mla: Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” Real Time
and Such, edited by Susanne Graf et al., vol. 15230, Springer Nature, 2024,
pp. 154–64, doi:10.1007/978-3-031-73751-0_12.
short: T.A. Henzinger, in:, S. Graf, P. Pettersson, B. Steffen (Eds.), Real Time
and Such, Springer Nature, Cham, 2024, pp. 154–164.
corr_author: '1'
date_created: 2024-11-18T09:10:06Z
date_published: 2024-10-23T00:00:00Z
date_updated: 2025-08-05T12:19:50Z
day: '23'
department:
- _id: ToHe
doi: 10.1007/978-3-031-73751-0_12
editor:
- first_name: Susanne
full_name: Graf, Susanne
last_name: Graf
- first_name: Paul
full_name: Pettersson, Paul
last_name: Pettersson
- first_name: Bernhard
full_name: Steffen, Bernhard
last_name: Steffen
intvolume: ' 15230'
language:
- iso: eng
month: '10'
oa_version: None
page: 154-164
place: Cham
publication: Real Time and Such
publication_identifier:
eisbn:
- '9783031737510'
eissn:
- 1611-3349
isbn:
- '9783031737503'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Reminiscences of a Real-Time Researcher
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15230
year: '2024'
...
---
OA_type: closed access
_id: '18599'
abstract:
- lang: eng
text: "Hypernode logic can reason about the prefix relation on stutter-reduced finite
traces through the stutter-reduced prefix predicate. We increase the expressiveness
of hypernode logic in two ways. First, we split the stutter-reduced prefix predicate
into an explicit stutter-reduction operator and the classical prefix predicate
on words. This change gives hypernode logic the ability to combine synchronous
and asynchronous reasoning by explicitly stating which parts of traces can stutter.
Second, we allow the use of regular expressions in formulas to reason about the
structure of traces. This change enables hypernode logic to describe a mixture
of trace properties and hyperproperties.\r\n\r\nWe show how to translate extended
hypernode logic formulas into multi-track automata, which are automata that read
multiple input words. Then we describe a fully online monitoring algorithm for
monitoring k-safety hyperproperties specified in the logic. We have implemented
the monitoring algorithm, and evaluated it on monitoring synchronous and asynchronous
versions of observational determinism, and on checking the privacy preservation
by compiler optimizations."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, and
by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- 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: 'Chalupa M, Henzinger TA, Oliveira da Costa A. Monitoring extended hypernode
logic. In: Integrated Formal Methods. Vol 15234. Springer Nature; 2024:151-171.
doi:10.1007/978-3-031-76554-4_9'
apa: Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. (2024). Monitoring
extended hypernode logic. In Integrated Formal Methods (Vol. 15234, pp.
151–171). Springer Nature. https://doi.org/10.1007/978-3-031-76554-4_9
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana Oliveira da Costa. “Monitoring
Extended Hypernode Logic.” In Integrated Formal Methods, 15234:151–71.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-76554-4_9.
ieee: M. Chalupa, T. A. Henzinger, and A. Oliveira da Costa, “Monitoring extended
hypernode logic,” in Integrated Formal Methods, 2024, vol. 15234, pp. 151–171.
ista: Chalupa M, Henzinger TA, Oliveira da Costa A. 2024. Monitoring extended hypernode
logic. Integrated Formal Methods. , LNCS, vol. 15234, 151–171.
mla: Chalupa, Marek, et al. “Monitoring Extended Hypernode Logic.” Integrated
Formal Methods, vol. 15234, Springer Nature, 2024, pp. 151–71, doi:10.1007/978-3-031-76554-4_9.
short: M. Chalupa, T.A. Henzinger, A. Oliveira da Costa, in:, Integrated Formal
Methods, Springer Nature, 2024, pp. 151–171.
corr_author: '1'
date_created: 2024-12-01T23:01:52Z
date_published: 2024-11-13T00:00:00Z
date_updated: 2025-09-08T14:47:22Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-031-76554-4_9
ec_funded: 1
external_id:
isi:
- '001416640500009'
intvolume: ' 15234'
isi: 1
language:
- iso: eng
month: '11'
oa_version: None
page: 151-171
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: Integrated Formal Methods
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031765537'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring extended hypernode logic
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15234
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '18600'
abstract:
- lang: eng
text: 'The analysis of formal models that include quantitative aspects such as timing
or probabilistic choices is performed by quantitative verification tools. Broad
and mature tool support is available for computing basic properties such as expected
rewards on basic models such as Markov chains. Previous editions of QComp, the
comparison of tools for the analysis of quantitative formal models, focused on
this setting. Many application scenarios, however, require more advanced property
types such as LTL and parameter synthesis queries as well as advanced models like
stochastic games and partially observable MDPs. For these, tool support is in
its infancy today. This paper presents the outcomes of QComp 2023: a survey of
the state of the art in quantitative verification tool support for advanced property
types and models. With tools ranging from first research prototypes to well-supported
integrations into established toolsets, this report highlights today’s active
areas and tomorrow’s challenges in tool-focused research for quantitative verification.'
acknowledgement: The authors are ordered alphabetically. This work was supported by
DFG RTG 2236/2 (UnRAVeL) and DFG project TRR 248 (CPEC, ID 389792660), by the EU
under MSCA grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199
(ProSVED), by ERC Starting Grant 101077178 (DEUCE), ERC Consolidator Grant 864075
(CAESAR), and ERC Advanced Grant 834115 (FUN2MODEL), by GAČR grant GA23-06963S (VESCAA),
by National Science Foundation grant 1856733, by NextGenerationEU project D53D23008400006
(SMARTITUDE), and by NWO VENI grant 639.021.754.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Roman
full_name: Andriushchenko, Roman
last_name: Andriushchenko
- first_name: Alexander
full_name: Bork, Alexander
last_name: Bork
- first_name: Carlos E.
full_name: Budde, Carlos E.
last_name: Budde
- first_name: Milan
full_name: Češka, Milan
last_name: Češka
- first_name: Kush
full_name: Grover, Kush
last_name: Grover
- first_name: Ernst Moritz
full_name: Hahn, Ernst Moritz
last_name: Hahn
- first_name: Arnd
full_name: Hartmanns, Arnd
last_name: Hartmanns
- first_name: Bryant
full_name: Israelsen, Bryant
last_name: Israelsen
- first_name: Nils
full_name: Jansen, Nils
last_name: Jansen
- first_name: Joshua
full_name: Jeppson, Joshua
last_name: Jeppson
- first_name: Sebastian
full_name: Junges, Sebastian
last_name: Junges
- first_name: Maximilian A.
full_name: Köhl, Maximilian A.
last_name: Köhl
- first_name: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Stefan
full_name: Pranger, Stefan
last_name: Pranger
- first_name: Tim
full_name: Quatmann, Tim
last_name: Quatmann
- first_name: Enno
full_name: Ruijters, Enno
last_name: Ruijters
- first_name: Landon
full_name: Taylor, Landon
last_name: Taylor
- first_name: Matthias
full_name: Volk, Matthias
last_name: Volk
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
- first_name: Zhen
full_name: Zhang, Zhen
last_name: Zhang
citation:
ama: 'Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report. In: TOOLympics Challenge 2023.
Vol 14550. Springer Nature; 2024:90-146. doi:10.1007/978-3-031-67695-6_4'
apa: 'Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E.
M., … Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification: QComp
2023 Competition Report. In TOOLympics Challenge 2023 (Vol. 14550, pp.
90–146). Springer Nature. https://doi.org/10.1007/978-3-031-67695-6_4'
chicago: 'Andriushchenko, Roman, Alexander Bork, Carlos E. Budde, Milan Češka, Kush
Grover, Ernst Moritz Hahn, Arnd Hartmanns, et al. “Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report.” In TOOLympics Challenge 2023,
14550:90–146. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-67695-6_4.'
ieee: 'R. Andriushchenko et al., “Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report,” in TOOLympics Challenge 2023,
2024, vol. 14550, pp. 90–146.'
ista: 'Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM, Hartmanns
A, Israelsen B, Jansen N, Jeppson J, Junges S, Köhl MA, Könighofer B, Kretinsky
J, Meggendorfer T, Parker D, Pranger S, Quatmann T, Ruijters E, Taylor L, Volk
M, Weininger M, Zhang Z. 2024. Tools at the Frontiers of Quantitative Verification:
QComp 2023 Competition Report. TOOLympics Challenge 2023. , LNCS, vol. 14550,
90–146.'
mla: 'Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification:
QComp 2023 Competition Report.” TOOLympics Challenge 2023, vol. 14550,
Springer Nature, 2024, pp. 90–146, doi:10.1007/978-3-031-67695-6_4.'
short: R. Andriushchenko, A. Bork, C.E. Budde, M. Češka, K. Grover, E.M. Hahn, A.
Hartmanns, B. Israelsen, N. Jansen, J. Jeppson, S. Junges, M.A. Köhl, B. Könighofer,
J. Kretinsky, T. Meggendorfer, D. Parker, S. Pranger, T. Quatmann, E. Ruijters,
L. Taylor, M. Volk, M. Weininger, Z. Zhang, in:, TOOLympics Challenge 2023, Springer
Nature, 2024, pp. 90–146.
date_created: 2024-12-01T23:01:53Z
date_published: 2024-11-01T00:00:00Z
date_updated: 2025-09-08T14:45:11Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-031-67695-6_4
external_id:
arxiv:
- '2405.13583'
isi:
- '001434957500004'
intvolume: ' 14550'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2405.13583'
month: '11'
oa: 1
oa_version: Preprint
page: 90-146
publication: TOOLympics Challenge 2023
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031676949'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition
Report'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14550
year: '2024'
...