---
OA_place: repository
OA_type: green
_id: '19712'
abstract:
- lang: eng
text: "We study recent algebraic attacks (Briaud-Øygarden EC’23) on the Regular
Syndrome Decoding (RSD) problem and the assumptions underlying the correctness
of their attacks’ complexity estimates. By relating these assumptions to interesting
algebraic-combinatorial problems, we prove that they do not hold in full generality.
However, we show that they are (asymptotically) true for most parameter sets,
supporting the soundness of algebraic attacks on RSD. Further, we prove—without
any heuristics or assumptions—that RSD can be broken in polynomial time whenever
the number of error blocks times the square of the size of error blocks is larger
than 2 times the square of the dimension of the code.\r\nAdditionally, we use
our methodology to attack a variant of the Learning With Errors problem where
each error term lies in a fixed set of constant size. We prove that this problem
can be broken in polynomial time, given a sufficient number of samples. This result
improves on the seminal work by Arora and Ge (ICALP’11), as the attack’s time
complexity is independent of the LWE modulus."
acknowledgement: We thank Pierre Briaud and Morten Øygarden for helpful discussions
on algebraic attacks on RSD, and the EC reviewers for helpful comments.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Simon-Philipp
full_name: Merz, Simon-Philipp
last_name: Merz
- first_name: Patrick
full_name: Stählin, Patrick
last_name: Stählin
- first_name: Akin
full_name: Ünal, Akin
id: f6b56fb6-dc63-11ee-9dbf-f6780863a85a
last_name: Ünal
orcid: 0000-0002-8929-0221
citation:
ama: 'Cueto Noval M, Merz S-P, Stählin P, Ünal A. On the soundness of algebraic
attacks against code-based assumptions. In: 44th Annual International Conference
on the Theory and Applications of Cryptographic Techniques. Vol 15606. Springer
Nature; 2025:385-415. doi:10.1007/978-3-031-91095-1_14'
apa: 'Cueto Noval, M., Merz, S.-P., Stählin, P., & Ünal, A. (2025). On the soundness
of algebraic attacks against code-based assumptions. In 44th Annual International
Conference on the Theory and Applications of Cryptographic Techniques (Vol.
15606, pp. 385–415). Madrid, Spain: Springer Nature. https://doi.org/10.1007/978-3-031-91095-1_14'
chicago: Cueto Noval, Miguel, Simon-Philipp Merz, Patrick Stählin, and Akin Ünal.
“On the Soundness of Algebraic Attacks against Code-Based Assumptions.” In 44th
Annual International Conference on the Theory and Applications of Cryptographic
Techniques, 15606:385–415. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-91095-1_14.
ieee: M. Cueto Noval, S.-P. Merz, P. Stählin, and A. Ünal, “On the soundness of algebraic
attacks against code-based assumptions,” in 44th Annual International Conference
on the Theory and Applications of Cryptographic Techniques, Madrid, Spain,
2025, vol. 15606, pp. 385–415.
ista: 'Cueto Noval M, Merz S-P, Stählin P, Ünal A. 2025. On the soundness of algebraic
attacks against code-based assumptions. 44th Annual International Conference on
the Theory and Applications of Cryptographic Techniques. EUROCRYPT: International
Conference on the Theory and Applications of Cryptographic Techniques, LNCS, vol.
15606, 385–415.'
mla: Cueto Noval, Miguel, et al. “On the Soundness of Algebraic Attacks against
Code-Based Assumptions.” 44th Annual International Conference on the Theory
and Applications of Cryptographic Techniques, vol. 15606, Springer Nature,
2025, pp. 385–415, doi:10.1007/978-3-031-91095-1_14.
short: M. Cueto Noval, S.-P. Merz, P. Stählin, A. Ünal, in:, 44th Annual International
Conference on the Theory and Applications of Cryptographic Techniques, Springer
Nature, 2025, pp. 385–415.
conference:
end_date: 2025-05-08
location: Madrid, Spain
name: 'EUROCRYPT: International Conference on the Theory and Applications of Cryptographic
Techniques'
start_date: 2025-05-04
corr_author: '1'
date_created: 2025-05-19T14:15:01Z
date_published: 2025-04-28T00:00:00Z
date_updated: 2025-05-28T06:12:39Z
day: '28'
department:
- _id: KrPi
doi: 10.1007/978-3-031-91095-1_14
fulldoi: https://doi.org/10.1007/978-3-031-91095-1_14
intvolume: ' 15606'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.research-collection.ethz.ch/handle/20.500.11850/732894
month: '04'
oa: 1
oa_version: Submitted Version
page: 385-415
publication: 44th Annual International Conference on the Theory and Applications of
Cryptographic Techniques
publication_identifier:
eisbn:
- '9783031910951'
eissn:
- 1611-3349
isbn:
- '9783031910944'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: On the soundness of algebraic attacks against code-based assumptions
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15606
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '19738'
abstract:
- lang: eng
text: "Garbling is a fundamental cryptographic primitive, with numerous theoretical
and practical applications. Since the first construction by Yao (FOCS’82, ’86),
a line of work has concerned itself with reducing the communication and computational
complexity of that construction. One of the most efficient garbling schemes presently
is the ‘Half Gates’ scheme by Zahur, Rosulek, and Evans (Eurocrypt’15). Despite
its widespread adoption, the provable security of this scheme has been based on
assumptions whose only instantiations are in idealized models. For example, in
their original paper, Zahur, Rosulek, and Evans showed that hash functions satisfying
a notion called circular correlation robustness (CCR) suffice for this task, and
then proved that CCR secure hash functions can be instantiated in the random permutation
model.\r\nIn this work, we show how to securely instantiate the Half Gates scheme
in the standard model. To this end, we first show how this scheme can be securely
instantiated given a (family of) weak CCR hash function, a notion that we introduce.
Furthermore, we show how a weak CCR hash function can be used to securely instantiate
other efficient garbling schemes, namely the ones by Rosulek and Roy (Crypto’21)
and Heath (Eurocrypt’24). Thus we believe this notion to be of independent interest.\r\nFinally,
we construct such weak CCR hash functions using indistinguishability obfuscation
and one-way functions. The security proof of this construction constitutes our
main technical contribution. While our construction is not practical, it serves
as a proof of concept supporting the soundness of these garbling schemes, which
we regard to be particularly important given the recent initiative by NIST to
standardize garbling, and the optimizations in Half Gates being potentially adopted."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Anasuya
full_name: Acharya, Anasuya
last_name: Acharya
- first_name: Karen
full_name: Azari, Karen
last_name: Azari
- first_name: Mirza Ahad
full_name: Baig, Mirza Ahad
id: 3EDE6DE4-AA5A-11E9-986D-341CE6697425
last_name: Baig
- first_name: Dennis
full_name: Hofheinz, Dennis
last_name: Hofheinz
- first_name: Chethan
full_name: Kamath, Chethan
last_name: Kamath
citation:
ama: 'Acharya A, Azari K, Baig MA, Hofheinz D, Kamath C. Securely instantiating
‘Half Gates’ garbling in the standard model. In: 28th IACR International Conference
on Practice and Theory of Public-Key Cryptography. Vol 15677. Springer Nature;
2025:37-75. doi:10.1007/978-3-031-91829-2_2'
apa: 'Acharya, A., Azari, K., Baig, M. A., Hofheinz, D., & Kamath, C. (2025).
Securely instantiating ‘Half Gates’ garbling in the standard model. In 28th
IACR International Conference on Practice and Theory of Public-Key Cryptography
(Vol. 15677, pp. 37–75). Roros, Norway: Springer Nature. https://doi.org/10.1007/978-3-031-91829-2_2'
chicago: Acharya, Anasuya, Karen Azari, Mirza Ahad Baig, Dennis Hofheinz, and Chethan
Kamath. “Securely Instantiating ‘Half Gates’ Garbling in the Standard Model.”
In 28th IACR International Conference on Practice and Theory of Public-Key
Cryptography, 15677:37–75. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-91829-2_2.
ieee: A. Acharya, K. Azari, M. A. Baig, D. Hofheinz, and C. Kamath, “Securely instantiating
‘Half Gates’ garbling in the standard model,” in 28th IACR International Conference
on Practice and Theory of Public-Key Cryptography, Roros, Norway, 2025, vol.
15677, pp. 37–75.
ista: 'Acharya A, Azari K, Baig MA, Hofheinz D, Kamath C. 2025. Securely instantiating
‘Half Gates’ garbling in the standard model. 28th IACR International Conference
on Practice and Theory of Public-Key Cryptography. PKC: Public-Key Cryptography,
LNCS, vol. 15677, 37–75.'
mla: Acharya, Anasuya, et al. “Securely Instantiating ‘Half Gates’ Garbling in the Standard
Model.” 28th IACR International Conference on Practice and Theory of Public-Key
Cryptography, vol. 15677, Springer Nature, 2025, pp. 37–75, doi:10.1007/978-3-031-91829-2_2.
short: A. Acharya, K. Azari, M.A. Baig, D. Hofheinz, C. Kamath, in:, 28th IACR International
Conference on Practice and Theory of Public-Key Cryptography, Springer Nature,
2025, pp. 37–75.
conference:
end_date: 2025-05-15
location: Roros, Norway
name: 'PKC: Public-Key Cryptography'
start_date: 2025-05-12
date_created: 2025-05-25T22:17:02Z
date_published: 2025-05-05T00:00:00Z
date_updated: 2025-06-02T07:01:45Z
day: '05'
department:
- _id: KrPi
- _id: GradSch
doi: 10.1007/978-3-031-91829-2_2
fulldoi: https://doi.org/10.1007/978-3-031-91829-2_2
intvolume: ' 15677'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2025/281
month: '05'
oa: 1
oa_version: Preprint
page: 37-75
publication: 28th IACR International Conference on Practice and Theory of Public-Key
Cryptography
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031918285'
issn:
- 0302-9743
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Securely instantiating ‘Half Gates’ garbling in the standard model
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15677
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19739'
abstract:
- lang: eng
text: "Cooperative verification is gaining momentum in recent years. The usual setup
in cooperative verification is that a verifier A is run with some pre-defined
resources, and if it is not able to verify the program, the verification task
is passed to a verifier B together with information learned about the program
by verifier A, then the chain can continue to a verifier C, and so on. This scheme
is static: tools run one after another in a fixed pre-defined order and fixed
parameters and resource limits (the scheme may differ for properties to be analyzed,
though).\r\n\r\nBubaak is a program analysis tool that allows to run multiple
program verifiers in a dynamically changing combination of parallel and sequential
portfolios. Bubaak starts the verification process by invoking an initial set
of tasks; every task, when it is done (e.g., because of hitting a time limit or
finishing its job), rewrites itself into one or more successor tasks. New tasks
can be also spawned upon events generated by other tasks. This all happens dynamically
based on the information gathered by finished and running tasks. During their
execution, tasks that run in parallel can exchange (partial) verification artifacts,
either directly or with Bubaak as an intermediary."
acknowledgement: This work was in part supported by the ERC-2020-AdG 10102009 grant,
and in part by the German Research Foundation (DFG) - WE2290/13-2 (Coop2).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Cedric
full_name: Richter, Cedric
last_name: Richter
citation:
ama: 'Chalupa M, Richter C. BUBAAK: Dynamic cooperative verification. In: 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. Vol 15698. Springer Nature; 2025:212-216. doi:10.1007/978-3-031-90660-2_14'
apa: 'Chalupa, M., & Richter, C. (2025). BUBAAK: Dynamic cooperative verification.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15698, pp. 212–216). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90660-2_14'
chicago: 'Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.”
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, 15698:212–16. Springer Nature, 2025. https://doi.org/10.1007/978-3-031-90660-2_14.'
ieee: 'M. Chalupa and C. Richter, “BUBAAK: Dynamic cooperative verification,” in
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Hamilton, ON, Canada, 2025, vol. 15698, pp. 212–216.'
ista: 'Chalupa M, Richter C. 2025. BUBAAK: Dynamic cooperative verification. 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
LNCS, vol. 15698, 212–216.'
mla: 'Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.”
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, vol. 15698, Springer Nature, 2025, pp. 212–16, doi:10.1007/978-3-031-90660-2_14.'
short: M. Chalupa, C. Richter, in:, 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 212–216.
conference:
end_date: 2025-05-08
location: Hamilton, ON, Canada
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2025-05-03
corr_author: '1'
date_created: 2025-05-25T22:17:04Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T07:21:41Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-90660-2_14
ec_funded: 1
file:
- access_level: open_access
checksum: 3f604f25dbe37383acb7f8308aad3ca6
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T07:10:35Z
date_updated: 2025-06-02T07:10:35Z
file_id: '19766'
file_name: 2025_TACAS_Chalupa.pdf
file_size: 259050
relation: main_file
success: 1
file_date_updated: 2025-06-02T07:10:35Z
fulldoi: https://doi.org/10.1007/978-3-031-90660-2_14
has_accepted_license: '1'
intvolume: ' 15698'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 212-216
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031906596'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'BUBAAK: Dynamic cooperative verification'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15698
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19742'
abstract:
- lang: eng
text: Statistical model checking estimates probabilities and expectations of interest
in probabilistic system models by using random simulations. Its results come with
statistical guarantees. However, many tools use unsound statistical methods that
produce incorrect results more often than they claim. In this paper, we provide
a comprehensive overview of tools and their correctness, as well as of sound methods
available for estimating probabilities from the literature. For expected rewards,
we investigate how to bound the path reward distribution to apply sound statistical
methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz
inequality that has not been used in SMC so far. We prove that even reachability
rewards can be bounded in theory, and formalise the concept of limit-PAC procedures
for a practical solution. The modes SMC tool implements our methods and recommendations,
which we use to experimentally confirm our results.
acknowledgement: This work was supported by the DFG through the Cluster of Excellence
EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy)
and the TRR 248 (see perspicuous-computing.science, project ID 389792660), by the
European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie
grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED),
by the EU under NextGenerationEU projects D53D23008400006 (Smartitude) under MUR
PRIN 2022 and PE00000014 (SERICS) under MUR PNRR, by the Interreg North Sea project
STORM_SAFE, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Carlos E.
full_name: Budde, Carlos E.
last_name: Budde
- first_name: Arnd
full_name: Hartmanns, Arnd
last_name: Hartmanns
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
- first_name: Patrick
full_name: Wienhöft, Patrick
last_name: Wienhöft
citation:
ama: 'Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical
model checking for probabilities and expected rewards. In: 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Vol 15696. Springer Nature; 2025:167-190. doi:10.1007/978-3-031-90643-5_9'
apa: 'Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., & Wienhöft,
P. (2025). Sound statistical model checking for probabilities and expected rewards.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90643-5_9'
chicago: Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger,
and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and
Expected Rewards.” In 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, 15696:167–90. Springer Nature,
2025. https://doi.org/10.1007/978-3-031-90643-5_9.
ieee: C. E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft,
“Sound statistical model checking for probabilities and expected rewards,” in
31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Hamilton, ON, Canada, 2025, vol. 15696, pp. 167–190.
ista: 'Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound
statistical model checking for probabilities and expected rewards. 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. 15696, 167–190.'
mla: Budde, Carlos E., et al. “Sound Statistical Model Checking for Probabilities
and Expected Rewards.” 31st International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, vol. 15696, Springer Nature,
2025, pp. 167–90, doi:10.1007/978-3-031-90643-5_9.
short: C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:,
31st International Conference on Tools and Algorithms for the Construction and
Analysis of Systems, Springer Nature, 2025, pp. 167–190.
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
date_created: 2025-05-25T22:17:08Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T09:45:41Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90643-5_9
ec_funded: 1
external_id:
arxiv:
- '2411.00559'
file:
- access_level: open_access
checksum: d45856b503b1dd4f8f14c3566327225b
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T09:35:42Z
date_updated: 2025-06-02T09:35:42Z
file_id: '19770'
file_name: 2025_TACAS_Budde.pdf
file_size: 711271
relation: main_file
success: 1
file_date_updated: 2025-06-02T09:35:42Z
fulldoi: https://doi.org/10.1007/978-3-031-90643-5_9
has_accepted_license: '1'
intvolume: ' 15696'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 167-190
project:
- _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:
- '9783031906428'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '19769'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Sound statistical model checking for probabilities and expected rewards
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
fulldoi: https://doi.org/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'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20189'
abstract:
- lang: eng
text: Certification was made mandatory for the first time in the latest hardware
model checking competition. In this case study, we investigate the trade-offs
of requiring certificates for both passing and failing properties in the competition.
Our evaluation shows that participating model checkers were able to produce compact,
correct certificates that could be verified with minimal overhead. Furthermore,
the certifying winner of the competition outperforms the previous non-certifying
state-of-the-art model checker, demonstrating that certification can be adopted
without compromising model checking efficiency.
acknowledgement: "This work is supported in part by the ERC-2020-AdG 101020093, the
LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland
under the project 336092, and a gift from Intel Corporation.\r\nFurthermore we of
course also owe a big thank-you to the submitters of model checkers and benchmarks
to the competition over all these years. Without their enthusiasm and support neither
the competition nor this study would exist."
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Nils
full_name: Froleyks, Nils
last_name: Froleyks
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
orcid: 0000-0002-4993-773X
- first_name: Mathias
full_name: Preiner, Mathias
last_name: Preiner
- first_name: Armin
full_name: Biere, Armin
last_name: Biere
- first_name: Keijo
full_name: Heljanko, Keijo
last_name: Heljanko
citation:
ama: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates
to the hardware model checking competition. In: 37th International Conference
on Computer Aided Verification. Vol 15931. Springer Nature; 2025:281-295.
doi:10.1007/978-3-031-98668-0_14'
apa: 'Froleyks, N., Yu, E., Preiner, M., Biere, A., & Heljanko, K. (2025). Introducing
certificates to the hardware model checking competition. In 37th International
Conference on Computer Aided Verification (Vol. 15931, pp. 281–295). Zagreb,
Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-98668-0_14'
chicago: Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko.
“Introducing Certificates to the Hardware Model Checking Competition.” In 37th
International Conference on Computer Aided Verification, 15931:281–95. Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-98668-0_14.
ieee: N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates
to the hardware model checking competition,” in 37th International Conference
on Computer Aided Verification, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.
ista: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates
to the hardware model checking competition. 37th International Conference on Computer
Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.'
mla: Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking
Competition.” 37th International Conference on Computer Aided Verification,
vol. 15931, Springer Nature, 2025, pp. 281–95, doi:10.1007/978-3-031-98668-0_14.
short: N. Froleyks, E. Yu, M. Preiner, A. Biere, K. Heljanko, in:, 37th International
Conference on Computer Aided Verification, Springer Nature, 2025, pp. 281–295.
conference:
end_date: 2025-07-25
location: Zagreb, Croatia
name: 'CAV: Computer Aided Verification'
start_date: 2025-07-23
date_created: 2025-08-17T22:01:36Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2025-12-01T12:34:05Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-98668-0_14
ec_funded: 1
external_id:
isi:
- '001562507100014'
file:
- access_level: open_access
checksum: 15ec1bc9b9409d3b2736f4c9d5f42fd1
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T05:46:10Z
date_updated: 2025-09-02T05:46:10Z
file_id: '20266'
file_name: 2025_CAV_Froleyks.pdf
file_size: 1078274
relation: main_file
success: 1
file_date_updated: 2025-09-02T05:46:10Z
fulldoi: https://doi.org/10.1007/978-3-031-98668-0_14
has_accepted_license: '1'
intvolume: ' 15931'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 281-295
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031986673'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Introducing certificates to the hardware model checking competition
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15931
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '20225'
abstract:
- lang: eng
text: "We present the first supermartingale certificate for quantitative \r\n-regular
properties of discrete-time infinite-state stochastic systems. Our certificate
is defined on the product of the stochastic system and a limit-deterministic Büchi
automaton that specifies the property of interest; hence we call it a limit-deterministic
Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied
only to quantitative reachability, safety, or reach-avoid properties, and to qualitative
(i.e., probability 1) \r\n-regular properties.We also present fully automated
algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic
system dynamics and the controller can be represented in terms of polynomial inequalities.
Our experiments demonstrate the ability of our method to solve verification and
control tasks for stochastic systems that were beyond the reach of previous supermartingale-based
approaches."
acknowledgement: This work was supported in part by the Singapore Ministry of Education
(MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SIS-SMU-100) and
the ERC project ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Pouya
full_name: Sadeghi, Pouya
last_name: Sadeghi
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Henzinger TA, Mallik K, Sadeghi P, Zikelic D. Supermartingale certificates
for quantitative omega-regular verification and control. In: 37th International
Conference on Computer Aided Verification. Vol 15932. Springer Nature; 2025:29-55.
doi:10.1007/978-3-031-98679-6_2'
apa: 'Henzinger, T. A., Mallik, K., Sadeghi, P., & Zikelic, D. (2025). Supermartingale
certificates for quantitative omega-regular verification and control. In 37th
International Conference on Computer Aided Verification (Vol. 15932, pp. 29–55).
Zagreb, Croatia: Springer Nature. https://doi.org/10.1007/978-3-031-98679-6_2'
chicago: Henzinger, Thomas A, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic.
“Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.”
In 37th International Conference on Computer Aided Verification, 15932:29–55.
Springer Nature, 2025. https://doi.org/10.1007/978-3-031-98679-6_2.
ieee: T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates
for quantitative omega-regular verification and control,” in 37th International
Conference on Computer Aided Verification, Zagreb, Croatia, 2025, vol. 15932,
pp. 29–55.
ista: 'Henzinger TA, Mallik K, Sadeghi P, Zikelic D. 2025. Supermartingale certificates
for quantitative omega-regular verification and control. 37th International Conference
on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15932,
29–55.'
mla: Henzinger, Thomas A., et al. “Supermartingale Certificates for Quantitative
Omega-Regular Verification and Control.” 37th International Conference on Computer
Aided Verification, vol. 15932, Springer Nature, 2025, pp. 29–55, doi:10.1007/978-3-031-98679-6_2.
short: T.A. Henzinger, K. Mallik, P. Sadeghi, D. Zikelic, in:, 37th International
Conference on Computer Aided Verification, Springer Nature, 2025, pp. 29–55.
conference:
end_date: 2025-07-25
location: Zagreb, Croatia
name: 'CAV: Computer Aided Verification'
start_date: 2025-07-23
date_created: 2025-08-24T22:01:31Z
date_published: 2025-07-22T00:00:00Z
date_updated: 2025-12-01T12:34:41Z
day: '22'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-98679-6_2
ec_funded: 1
external_id:
arxiv:
- '2505.18833'
isi:
- '001562506600002'
file:
- access_level: open_access
checksum: beb1e2637de5b2268cc2262119439113
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T07:34:33Z
date_updated: 2025-09-02T07:34:33Z
file_id: '20272'
file_name: 2025_CAV_HenzingerT.pdf
file_size: 884831
relation: main_file
success: 1
file_date_updated: 2025-09-02T07:34:33Z
fulldoi: https://doi.org/10.1007/978-3-031-98679-6_2
has_accepted_license: '1'
intvolume: ' 15932'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 29-55
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031986789'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Supermartingale certificates for quantitative omega-regular verification and control
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15932
year: '2025'
...
---
_id: '20610'
abstract:
- lang: eng
text: "Markov decision processes (MDPs) are a fundamental model of decision making
which exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally,
verification assumes exact knowledge of the probabilities that govern the behaviour
of an MDP. However, this assumption often is unrealistic, e.g. when modelling
cyber-physical systems or biological processes. There, we can employ statistical
model checking (SMC) to obtain an estimate of the MDP’s value (e.g. the maximal
probability of reaching a goal state) that is close to the true value with high
confidence (probably approximately correct). Model-based SMC algorithms sample
the MDP and build a model of it by estimating all transition probabilities, essentially
for every transition answering the question: “What are the odds?” However, so
far the statistical methods employed by state-of-the-art SMC verification algorithms
are quite naive or even compromise the correctness guarantees.\r\n\r\nOur first
contribution is to survey, categorize, and analyse statistical methods, identifying
those few that are most efficient and that provide suitable guarantees for the
verification setting. Secondly, we propose improvements that exploit structural
knowledge of the MDP. Both contributions generalize to many types of problem statements
as they are largely independent of the setting. Moreover, our experimental evaluation
shows that they lead to significant gains, reducing the number of samples that
an SMC algorithm has to collect by up to two orders of magnitude."
acknowledgement: This work was supported by the European Union’s Horizon 2020 research
and innovation programme under the Marie Sklodowska-Curie grant agreement No 10103441,
the ERC Starting Grant DEUCE (101077178) and the DFG through the Cluster of Excellence
EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy)
and the DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
orcid: 0000-0002-0163-2152
- first_name: Patrick
full_name: Wienhöft, Patrick
last_name: Wienhöft
citation:
ama: 'Meggendorfer T, Weininger M, Wienhöft P. What are the odds? Improving statistical
model checking of Markov decision processes. In: Second International Joint
Conference on QEST+FORMATS. Vol 16143. Springer Nature; 2025:195-218. doi:10.1007/978-3-032-05792-1_11'
apa: 'Meggendorfer, T., Weininger, M., & Wienhöft, P. (2025). What are the odds?
Improving statistical model checking of Markov decision processes. In Second
International Joint Conference on QEST+FORMATS (Vol. 16143, pp. 195–218).
Aarhus, Denmark: Springer Nature. https://doi.org/10.1007/978-3-032-05792-1_11'
chicago: Meggendorfer, Tobias, Maximilian Weininger, and Patrick Wienhöft. “What
Are the Odds? Improving Statistical Model Checking of Markov Decision Processes.”
In Second International Joint Conference on QEST+FORMATS, 16143:195–218.
Springer Nature, 2025. https://doi.org/10.1007/978-3-032-05792-1_11.
ieee: T. Meggendorfer, M. Weininger, and P. Wienhöft, “What are the odds? Improving
statistical model checking of Markov decision processes,” in Second International
Joint Conference on QEST+FORMATS, Aarhus, Denmark, 2025, vol. 16143, pp. 195–218.
ista: 'Meggendorfer T, Weininger M, Wienhöft P. 2025. What are the odds? Improving
statistical model checking of Markov decision processes. Second International
Joint Conference on QEST+FORMATS. QEST-FORMATS: International Conference on Quantitative
Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, LNCS,
vol. 16143, 195–218.'
mla: Meggendorfer, Tobias, et al. “What Are the Odds? Improving Statistical Model
Checking of Markov Decision Processes.” Second International Joint Conference
on QEST+FORMATS, vol. 16143, Springer Nature, 2025, pp. 195–218, doi:10.1007/978-3-032-05792-1_11.
short: T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Second International Joint
Conference on QEST+FORMATS, Springer Nature, 2025, pp. 195–218.
conference:
end_date: 2025-08-28
location: Aarhus, Denmark
name: 'QEST-FORMATS: International Conference on Quantitative Evaluation of Systems
and Formal Modeling and Analysis of Timed Systems'
start_date: 2025-08-26
date_created: 2025-11-09T23:01:34Z
date_published: 2025-10-02T00:00:00Z
date_updated: 2025-11-10T08:06:27Z
day: '02'
department:
- _id: KrCh
doi: 10.1007/978-3-032-05792-1_11
ec_funded: 1
fulldoi: https://doi.org/10.1007/978-3-032-05792-1_11
intvolume: ' 16143'
language:
- iso: eng
month: '10'
oa_version: None
page: 195-218
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Second International Joint Conference on QEST+FORMATS
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032057914'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: What are the odds? Improving statistical model checking of Markov decision
processes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16143
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20658'
abstract:
- lang: eng
text: The medial axis of a smoothly embedded surface in R^3 consists of all points
for which the Euclidean distance function on the surface has at least two global
minima. We generalize this notion to the mid-sphere axis, which consists of all
points for which the Euclidean distance function has two interchanging saddles
that swap their partners in the pairing by persistent homology. It offers a discrete-algebraic
multi-scale approach to computing ridge-like structures on the surface. As a proof
of concept, an algorithm that computes stair-case approximations of the mid-sphere
axis is provided.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Elizabeth R
full_name: Stephenson, Elizabeth R
id: 2D04F932-F248-11E8-B48F-1D18A9856A87
last_name: Stephenson
orcid: 0000-0002-6862-208X
- first_name: Martin H
full_name: Thoresen, Martin H
id: 47CB1472-F248-11E8-B48F-1D18A9856A87
last_name: Thoresen
citation:
ama: 'Edelsbrunner H, Stephenson ER, Thoresen MH. The mid-sphere cousin of the medial
axis transform. In: 4th International Joint Conference on Discrete Geometry
and Mathematical Morphology. Vol 16296. Springer Nature; 2025:133-147. doi:10.1007/978-3-032-09544-2_10'
apa: 'Edelsbrunner, H., Stephenson, E. R., & Thoresen, M. H. (2025). The mid-sphere
cousin of the medial axis transform. In 4th International Joint Conference
on Discrete Geometry and Mathematical Morphology (Vol. 16296, pp. 133–147).
Groningen, The Netherlands: Springer Nature. https://doi.org/10.1007/978-3-032-09544-2_10'
chicago: Edelsbrunner, Herbert, Elizabeth R Stephenson, and Martin H Thoresen. “The
Mid-Sphere Cousin of the Medial Axis Transform.” In 4th International Joint
Conference on Discrete Geometry and Mathematical Morphology, 16296:133–47.
Springer Nature, 2025. https://doi.org/10.1007/978-3-032-09544-2_10.
ieee: H. Edelsbrunner, E. R. Stephenson, and M. H. Thoresen, “The mid-sphere cousin
of the medial axis transform,” in 4th International Joint Conference on Discrete
Geometry and Mathematical Morphology, Groningen, The Netherlands, 2025, vol.
16296, pp. 133–147.
ista: 'Edelsbrunner H, Stephenson ER, Thoresen MH. 2025. The mid-sphere cousin of the medial
axis transform. 4th International Joint Conference on Discrete Geometry and Mathematical
Morphology. DGMM: Discrete Geometry and Mathematical Morphology, LNCS, vol. 16296,
133–147.'
mla: Edelsbrunner, Herbert, et al. “The Mid-Sphere Cousin of the Medial Axis Transform.”
4th International Joint Conference on Discrete Geometry and Mathematical Morphology,
vol. 16296, Springer Nature, 2025, pp. 133–47, doi:10.1007/978-3-032-09544-2_10.
short: H. Edelsbrunner, E.R. Stephenson, M.H. Thoresen, in:, 4th International Joint
Conference on Discrete Geometry and Mathematical Morphology, Springer Nature,
2025, pp. 133–147.
conference:
end_date: 2025-11-06
location: Groningen, The Netherlands
name: 'DGMM: Discrete Geometry and Mathematical Morphology'
start_date: 2025-11-03
date_created: 2025-11-23T23:01:37Z
date_published: 2025-11-01T00:00:00Z
date_updated: 2025-11-24T10:05:11Z
day: '01'
department:
- _id: HeEd
doi: 10.1007/978-3-032-09544-2_10
external_id:
arxiv:
- '2504.14743'
fulldoi: https://doi.org/10.1007/978-3-032-09544-2_10
intvolume: ' 16296'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2504.14743
month: '11'
oa: 1
oa_version: Preprint
page: 133-147
publication: 4th International Joint Conference on Discrete Geometry and Mathematical
Morphology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032095435'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: The mid-sphere cousin of the medial axis transform
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16296
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20723'
abstract:
- lang: eng
text: Information-flow interfaces is a formalism recently proposed for specifying,
composing, and refining system-wide security requirements. In this work, we show
how the widely used concept of security lattices provides a natural semantic interpretation
for information-flow interfaces.
acknowledgement: This project was funded in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe F8502 and by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-Flow
Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber
Physical Systems. Vol 15471. Cham: Springer Nature; 2025:251-263. doi:10.1007/978-3-031-97537-0_15'
apa: 'Bartocci, E., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A.
(2025). Information-Flow Interfaces and Security Lattices. In Engineering Safe
and Trustworthy Cyber Physical Systems (Vol. 15471, pp. 251–263). Cham: Springer
Nature. https://doi.org/10.1007/978-3-031-97537-0_15'
chicago: 'Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da
Costa. “Information-Flow Interfaces and Security Lattices.” In Engineering
Safe and Trustworthy Cyber Physical Systems, 15471:251–63. Cham: Springer
Nature, 2025. https://doi.org/10.1007/978-3-031-97537-0_15.'
ieee: 'E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-Flow
Interfaces and Security Lattices,” in Engineering Safe and Trustworthy Cyber
Physical Systems, vol. 15471, Cham: Springer Nature, 2025, pp. 251–263.'
ista: 'Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.Information-Flow
Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber Physical
Systems. LNCS, vol. 15471, 251–263.'
mla: Bartocci, Ezio, et al. “Information-Flow Interfaces and Security Lattices.”
Engineering Safe and Trustworthy Cyber Physical Systems, vol. 15471, Springer
Nature, 2025, pp. 251–63, doi:10.1007/978-3-031-97537-0_15.
short: E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, Engineering
Safe and Trustworthy Cyber Physical Systems, Springer Nature, Cham, 2025, pp.
251–263.
corr_author: '1'
date_created: 2025-12-01T15:44:58Z
date_published: 2025-10-02T00:00:00Z
date_updated: 2025-12-09T07:57:55Z
day: '02'
department:
- _id: ToHe
doi: 10.1007/978-3-031-97537-0_15
ec_funded: 1
external_id:
arxiv:
- '2406.14374'
fulldoi: https://doi.org/10.1007/978-3-031-97537-0_15
intvolume: ' 15471'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2406.14374
month: '10'
oa: 1
oa_version: Preprint
page: 251-263
place: Cham
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Engineering Safe and Trustworthy Cyber Physical Systems
publication_identifier:
eisbn:
- '9783031975370'
eissn:
- 1611-3349
isbn:
- '9783031975363'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Information-Flow Interfaces and Security Lattices
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15471
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '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'
cryptoeprintid: 1
das_tickbox: '1'
date_created: 2025-12-21T23:01:33Z
date_published: 2025-12-05T00:00:00Z
date_updated: 2026-07-21T09:17:38Z
day: '05'
department:
- _id: KrPi
doi: 10.1007/978-3-032-12290-2_6
external_id:
cryptoeprintid:
- 2025/1723
fulldoi: https://doi.org/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: 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-07-27T12:48:18Z
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
fulldoi: https://doi.org/10.1007/978-3-031-90643-5_16
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: '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-08-21T10:53:16Z
day: '17'
department:
- _id: KrPi
doi: 10.1007/978-3-032-01913-4_5
fulldoi: https://doi.org/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'
related_material:
record:
- id: '22664'
relation: dissertation_contains
status: public
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: 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
orcid: 0000-0002-0163-2152
- 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: 2026-09-16T06:57:17Z
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
fulldoi: https://doi.org/10.1007/978-3-031-90653-4_7
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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: '19740'
abstract:
- lang: eng
text: Two standard models for probabilistic systems are Markov chains (MCs) and
Markov decision processes (MDPs). Classic objectives for such probabilistic models
for control and planning problems are reachability and stochastic shortest path.
The widely studied algorithmic approach for these problems is the Value Iteration
(VI) algorithm which iteratively applies local updates called Bellman updates.
There are many practical approaches for VI in the literature but they all require
exponentially many Bellman updates for MCs in the worst case. A preprocessing
step is an algorithm that is discrete, graph-theoretical, and requires linear
space. An important open question is whether, after a polynomial-time preprocessing,
VI can be achieved with sub-exponentially many Bellman updates. In this work,
we present a new approach for VI based on guessing values. Our theoretical contributions
are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm
after which, along with guessing values, VI requires only subexponentially many
Bellman updates. Second, we present an improved analysis of the speed of convergence
of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our
new approach. Experimental results show that our approach provides a considerable
improvement over existing VI-based approaches on several benchmark examples from
the literature.
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt)
grant and Austrian Science Fund (FWF) 10.55776/COE12 grant.
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: Mahdi
full_name: Jafariraviz, Mahdi
last_name: Jafariraviz
- first_name: Raimundo J
full_name: Saona Urmeneta, Raimundo J
id: BD1DF4C4-D767-11E9-B658-BC13E6697425
last_name: Saona Urmeneta
orcid: 0000-0001-5103-038X
- first_name: Jakub
full_name: Svoboda, Jakub
id: 130759D2-D7DD-11E9-87D2-DE0DE6697425
last_name: Svoboda
orcid: 0000-0002-1419-3267
citation:
ama: 'Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. Value iteration
with guessing for Markov chains and Markov decision processes. In: 31st International
Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Vol 15697. Springer Nature; 2025:217-236. doi:10.1007/978-3-031-90653-4_11'
apa: 'Chatterjee, K., Jafariraviz, M., Saona Urmeneta, R. J., & Svoboda, J.
(2025). Value iteration with guessing for Markov chains and Markov decision processes.
In 31st International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 15697, pp. 217–236). Hamilton, ON, Canada: Springer
Nature. https://doi.org/10.1007/978-3-031-90653-4_11'
chicago: Chatterjee, Krishnendu, Mahdi Jafariraviz, Raimundo J Saona Urmeneta, and
Jakub Svoboda. “Value Iteration with Guessing for Markov Chains and Markov Decision
Processes.” In 31st International Conference on Tools and Algorithms for the
Construction and Analysis of Systems, 15697:217–36. Springer Nature, 2025.
https://doi.org/10.1007/978-3-031-90653-4_11.
ieee: K. Chatterjee, M. Jafariraviz, R. J. Saona Urmeneta, and J. Svoboda, “Value
iteration with guessing for Markov chains and Markov decision processes,” in 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, Hamilton, ON, Canada, 2025, vol. 15697, pp. 217–236.
ista: 'Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. 2025. Value iteration
with guessing for Markov chains and Markov decision processes. 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, 217–236.'
mla: Chatterjee, Krishnendu, et al. “Value Iteration with Guessing for Markov Chains
and Markov Decision Processes.” 31st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, vol. 15697, Springer
Nature, 2025, pp. 217–36, doi:10.1007/978-3-031-90653-4_11.
short: K. Chatterjee, M. Jafariraviz, R.J. Saona Urmeneta, J. Svoboda, in:, 31st
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, Springer Nature, 2025, pp. 217–236.
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:06Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2026-09-16T06:56:56Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90653-4_11
ec_funded: 1
external_id:
arxiv:
- '2505.06769'
file:
- access_level: open_access
checksum: 45da6efbcbed20aada16c48c8e55e2d6
content_type: application/pdf
creator: dernst
date_created: 2025-06-02T07:31:12Z
date_updated: 2025-06-02T07:31:12Z
file_id: '19767'
file_name: 2025_TACAS_Chatterjee.pdf
file_size: 557481
relation: main_file
success: 1
file_date_updated: 2025-06-02T07:31:12Z
fulldoi: https://doi.org/10.1007/978-3-031-90653-4_11
has_accepted_license: '1'
intvolume: ' 15697'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 217-236
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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: Value iteration with guessing for Markov chains and Markov decision processes
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: 2026-09-16T06:57:43Z
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
fulldoi: https://doi.org/10.1007/978-3-031-90653-4_14
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'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
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: '20648'
abstract:
- lang: eng
text: Polynomial quantified entailments with existentially and universally quantified
variables arise in many problems of verification and program analysis. We present
PolyQEnt which is a tool for solving polynomial quantified entailments in which
variables on both sides of the implication are real valued or unbounded integers.
Our tool provides a unified framework for polynomial quantified entailment problems
that arise in several papers in the literature. Our experimental evaluation over
a wide range of benchmarks shows the applicability of the tool as well as its
benefits as opposed to simply using existing SMT solvers to solve such constraints.
acknowledgement: 'This work was supported by the following grants: ERC CoG 863818
(ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, ERC StG 101222524 (SPES),
the Ethereum Foundation Research Grant FY24-1793, and the Singapore Ministry of
Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SISSMU-100).'
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: 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: Kafshdar Goharshadi, Ehsan
id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
last_name: Kafshdar Goharshadi
orcid: 0000-0002-8595-0587
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
orcid: 0009-0007-5253-9170
- first_name: Milad
full_name: Saadat, Milad
last_name: Saadat
- first_name: Maximilian
full_name: Seeliger, Maximilian
last_name: Seeliger
- 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, et al. PolyQEnt: A polynomial quantified
entailment solver. In: 23rd International Symposium on Automated Technology
for Verification and Analysis. Vol 16145. Springer Nature; 2025:411-424. doi:10.1007/978-3-032-08707-2_19'
apa: 'Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., Saadat, M.,
Seeliger, M., & Zikelic, D. (2025). PolyQEnt: A polynomial quantified entailment
solver. In 23rd International Symposium on Automated Technology for Verification
and Analysis (Vol. 16145, pp. 411–424). Bengaluru, India: Springer Nature.
https://doi.org/10.1007/978-3-032-08707-2_19'
chicago: 'Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad
Karrabi, Milad Saadat, Maximilian Seeliger, and Dorde Zikelic. “PolyQEnt: A Polynomial
Quantified Entailment Solver.” In 23rd International Symposium on Automated
Technology for Verification and Analysis, 16145:411–24. Springer Nature, 2025.
https://doi.org/10.1007/978-3-032-08707-2_19.'
ieee: 'K. Chatterjee et al., “PolyQEnt: A polynomial quantified entailment
solver,” in 23rd International Symposium on Automated Technology for Verification
and Analysis, Bengaluru, India, 2025, vol. 16145, pp. 411–424.'
ista: 'Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Saadat M, Seeliger
M, Zikelic D. 2025. PolyQEnt: A polynomial quantified entailment solver. 23rd
International Symposium on Automated Technology for Verification and Analysis.
ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 16145, 411–424.'
mla: 'Chatterjee, Krishnendu, et al. “PolyQEnt: A Polynomial Quantified Entailment
Solver.” 23rd International Symposium on Automated Technology for Verification
and Analysis, vol. 16145, Springer Nature, 2025, pp. 411–24, doi:10.1007/978-3-032-08707-2_19.'
short: K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, M. Saadat, M.
Seeliger, D. Zikelic, in:, 23rd International Symposium on Automated Technology
for Verification and Analysis, Springer Nature, 2025, pp. 411–424.
conference:
end_date: 2025-10-31
location: Bengaluru, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2025-10-27
corr_author: '1'
date_created: 2025-11-16T23:01:24Z
date_published: 2025-10-26T00:00:00Z
date_updated: 2026-09-16T07:03:56Z
day: '26'
department:
- _id: KrCh
doi: 10.1007/978-3-032-08707-2_19
ec_funded: 1
external_id:
arxiv:
- '2408.03796'
fulldoi: https://doi.org/10.1007/978-3-032-08707-2_19
intvolume: ' 16145'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2408.03796
month: '10'
oa: 1
oa_version: Preprint
page: 411-424
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 4029cfc7-b034-11f1-9e55-88ab2ff3b6ee
grant_number: COE12
name: Bilateral Artificial Intelligence (Chatterjee)
publication: 23rd International Symposium on Automated Technology for Verification
and Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032087065'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'PolyQEnt: A polynomial quantified entailment solver'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16145
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-09-18T07:41:29Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-032-05435-7_1
ec_funded: 1
external_id:
arxiv:
- '2507.20711'
fulldoi: https://doi.org/10.1007/978-3-032-05435-7_1
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'
related_material:
record:
- id: '22808'
relation: dissertation_contains
status: public
status: public
title: 'Algorithmic fairness: A runtime perspective'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16087
year: '2025'
...
---
_id: '14888'
abstract:
- lang: eng
text: 'A face in a curve arrangement is called popular if it is bounded by the same
curve multiple times. Motivated by the automatic generation of curved nonogram
puzzles, we investigate possibilities to eliminate the popular faces in an arrangement
by inserting a single additional curve. This turns out to be NP-hard; however,
it becomes tractable when the number of popular faces is small: We present a probabilistic
FPT-approach in the number of popular faces.'
acknowledgement: 'This work was initiated at the 16th European Research Week on Geometric
Graphs in Strobl in 2019. A.W. is supported by the Austrian Science Fund (FWF):
W1230. S.T. has been funded by the Vienna Science and Technology Fund (WWTF) [10.47379/ICT19035].
A preliminary version of this work has been presented at the 38th European Workshop
on Computational Geometry (EuroCG 2022) in Perugia [9]. A full version of this paper,
which includes appendices but is otherwise identical, is available as a technical
report [10].'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Phoebe
full_name: De Nooijer, Phoebe
last_name: De Nooijer
- first_name: Soeren
full_name: Terziadis, Soeren
last_name: Terziadis
- first_name: Alexandra
full_name: Weinberger, Alexandra
last_name: Weinberger
- first_name: Zuzana
full_name: Masárová, Zuzana
id: 45CFE238-F248-11E8-B48F-1D18A9856A87
last_name: Masárová
orcid: 0000-0002-6660-1322
- first_name: Tamara
full_name: Mchedlidze, Tamara
last_name: Mchedlidze
- first_name: Maarten
full_name: Löffler, Maarten
last_name: Löffler
- first_name: Günter
full_name: Rote, Günter
last_name: Rote
citation:
ama: 'De Nooijer P, Terziadis S, Weinberger A, et al. Removing popular faces in curve
arrangements. In: 31st International Symposium on Graph Drawing and Network
Visualization. Vol 14466. Springer Nature; 2024:18-33. doi:10.1007/978-3-031-49275-4_2'
apa: 'De Nooijer, P., Terziadis, S., Weinberger, A., Masárová, Z., Mchedlidze, T.,
Löffler, M., & Rote, G. (2024). Removing popular faces in curve arrangements.
In 31st International Symposium on Graph Drawing and Network Visualization
(Vol. 14466, pp. 18–33). Isola delle Femmine, Palermo, Italy: Springer Nature.
https://doi.org/10.1007/978-3-031-49275-4_2'
chicago: De Nooijer, Phoebe, Soeren Terziadis, Alexandra Weinberger, Zuzana Masárová,
Tamara Mchedlidze, Maarten Löffler, and Günter Rote. “Removing Popular Faces in Curve
Arrangements.” In 31st International Symposium on Graph Drawing and Network
Visualization, 14466:18–33. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-49275-4_2.
ieee: P. De Nooijer et al., “Removing popular faces in curve arrangements,”
in 31st International Symposium on Graph Drawing and Network Visualization,
Isola delle Femmine, Palermo, Italy, 2024, vol. 14466, pp. 18–33.
ista: 'De Nooijer P, Terziadis S, Weinberger A, Masárová Z, Mchedlidze T, Löffler
M, Rote G. 2024. Removing popular faces in curve arrangements. 31st International
Symposium on Graph Drawing and Network Visualization. GD: Graph Drawing and Network
Visualization, LNCS, vol. 14466, 18–33.'
mla: De Nooijer, Phoebe, et al. “Removing Popular Faces in Curve Arrangements.”
31st International Symposium on Graph Drawing and Network Visualization,
vol. 14466, Springer Nature, 2024, pp. 18–33, doi:10.1007/978-3-031-49275-4_2.
short: P. De Nooijer, S. Terziadis, A. Weinberger, Z. Masárová, T. Mchedlidze, M.
Löffler, G. Rote, in:, 31st International Symposium on Graph Drawing and Network
Visualization, Springer Nature, 2024, pp. 18–33.
conference:
end_date: 2023-09-22
location: Isola delle Femmine, Palermo, Italy
name: 'GD: Graph Drawing and Network Visualization'
start_date: 2023-09-20
date_created: 2024-01-28T23:01:43Z
date_published: 2024-01-06T00:00:00Z
date_updated: 2025-09-04T11:52:35Z
day: '06'
department:
- _id: UlWa
- _id: HeEd
doi: 10.1007/978-3-031-49275-4_2
external_id:
arxiv:
- '2202.12175'
isi:
- '001207942000002'
fulldoi: https://doi.org/10.1007/978-3-031-49275-4_2
intvolume: ' 14466'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2202.12175
month: '01'
oa: 1
oa_version: Preprint
page: 18-33
publication: 31st International Symposium on Graph Drawing and Network Visualization
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031492747'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Removing popular faces in curve arrangements
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14466
year: '2024'
...
---
_id: '15012'
abstract:
- lang: eng
text: We solve a problem of Dujmović and Wood (2007) by showing that a complete
convex geometric graph on n vertices cannot be decomposed into fewer than n-1
star-forests, each consisting of noncrossing edges. This bound is clearly tight.
We also discuss similar questions for abstract graphs.
acknowledgement: János Pach’s Research partially supported by European Research Council
(ERC), grant “GeoScape” No. 882971 and by the Hungarian Science Foundation (NKFIH),
grant K-131529. Work by Morteza Saghafian is partially supported by the European
Research Council (ERC), grant No. 788183, and by the Wittgenstein Prize, Austrian
Science Fund (FWF), grant No. Z 342-N31.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: János
full_name: Pach, János
id: E62E3130-B088-11EA-B919-BF823C25FEA4
last_name: Pach
- first_name: Morteza
full_name: Saghafian, Morteza
id: f86f7148-b140-11ec-9577-95435b8df824
last_name: Saghafian
- first_name: Patrick
full_name: Schnider, Patrick
last_name: Schnider
citation:
ama: 'Pach J, Saghafian M, Schnider P. Decomposition of geometric graphs into star-forests.
In: 31st International Symposium on Graph Drawing and Network Visualization.
Vol 14465. Springer Nature; 2024:339-346. doi:10.1007/978-3-031-49272-3_23'
apa: 'Pach, J., Saghafian, M., & Schnider, P. (2024). Decomposition of geometric
graphs into star-forests. In 31st International Symposium on Graph Drawing
and Network Visualization (Vol. 14465, pp. 339–346). Isola delle Femmine,
Palermo, Italy: Springer Nature. https://doi.org/10.1007/978-3-031-49272-3_23'
chicago: Pach, János, Morteza Saghafian, and Patrick Schnider. “Decomposition of Geometric
Graphs into Star-Forests.” In 31st International Symposium on Graph Drawing
and Network Visualization, 14465:339–46. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-49272-3_23.
ieee: J. Pach, M. Saghafian, and P. Schnider, “Decomposition of geometric graphs
into star-forests,” in 31st International Symposium on Graph Drawing and Network
Visualization, Isola delle Femmine, Palermo, Italy, 2024, vol. 14465, pp.
339–346.
ista: 'Pach J, Saghafian M, Schnider P. 2024. Decomposition of geometric graphs
into star-forests. 31st International Symposium on Graph Drawing and Network Visualization.
GD: Graph Drawing and Network Visualization, LNCS, vol. 14465, 339–346.'
mla: Pach, János, et al. “Decomposition of Geometric Graphs into Star-Forests.”
31st International Symposium on Graph Drawing and Network Visualization,
vol. 14465, Springer Nature, 2024, pp. 339–46, doi:10.1007/978-3-031-49272-3_23.
short: J. Pach, M. Saghafian, P. Schnider, in:, 31st International Symposium on
Graph Drawing and Network Visualization, Springer Nature, 2024, pp. 339–346.
conference:
end_date: 2023-09-22
location: Isola delle Femmine, Palermo, Italy
name: 'GD: Graph Drawing and Network Visualization'
start_date: 2023-09-20
date_created: 2024-02-18T23:01:03Z
date_published: 2024-01-01T00:00:00Z
date_updated: 2026-04-16T09:12:37Z
day: '01'
department:
- _id: HeEd
doi: 10.1007/978-3-031-49272-3_23
ec_funded: 1
external_id:
arxiv:
- '2306.13201'
isi:
- '001207939600023'
fulldoi: https://doi.org/10.1007/978-3-031-49272-3_23
intvolume: ' 14465'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2306.13201
month: '01'
oa: 1
oa_version: Preprint
page: 339-346
project:
- _id: 266A2E9E-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '788183'
name: Alpha Shape Theory Extended
- _id: 268116B8-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z00342
name: Mathematics, Computer Science
publication: 31st International Symposium on Graph Drawing and Network Visualization
publication_identifier:
eisbn:
- '9783031492723'
eissn:
- 1611-3349
isbn:
- '9783031492716'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '21253'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Decomposition of geometric graphs into star-forests
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 14465
year: '2024'
...