---
_id: '17126'
abstract:
- lang: eng
text: "Functional encryption (FE) is a primitive where the holder of a master secret
key can control which functions a user can evaluate on encrypted data. It is a
powerful primitive that even implies indistinguishability obfuscation (iO), given
sufficiently compact ciphertexts (Ananth-Jain, CRYPTO’15 and Bitansky-Vaikuntanathan,
FOCS’15). However, despite being extensively studied, there are FE schemes, such
as function-hiding inner-product FE (Bishop-Jain-Kowalczyk, AC’15, Abdalla-Catalano-Fiore-Gay-Ursu,
CRYPTO’18) and compact quadratic FE (Baltico-Catalano-Fiore-Gay, Lin, CRYPTO’17),
that can be only realized using pairings. This raises the question if there are
some mathematical barriers that hinder us from realizing these FE schemes from
other assumptions.\r\n\r\nIn this paper, we study the difficulty of constructing
lattice-based compact FE. We generalize the impossibility results of Ünal (EC’20)
for lattice-based function-hiding FE, and extend it to the case of compact FE.
Concretely, we prove lower bounds for lattice-based compact FE schemes which meet
some (natural) algebraic restrictions at encryption and decryption, and have ciphertexts
of linear size and secret keys of minimal degree. We see our results as important
indications of why it is hard to construct lattice-based FE schemes for new functionalities,
and which mathematical barriers have to be overcome."
acknowledgement: We want to thank the anonymous reviewers of TCC and Eurocrypt for
their very helpful comments and suggestions. This work has received funding from
the Austrian Science Fund (FWF) and netidee SCIENCE via grant P31621-N38 (PROFET).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Erkan
full_name: Tairi, Erkan
last_name: Tairi
- first_name: Akin
full_name: Ünal, Akin
id: f6b56fb6-dc63-11ee-9dbf-f6780863a85a
last_name: Ünal
orcid: 0000-0002-8929-0221
citation:
ama: 'Tairi E, Ünal A. Lower bounds for lattice-based compact functional encryption.
In: Advances in Cryptology – EUROCRYPT 2024. Vol 14652. Springer Nature;
2024:249-279. doi:10.1007/978-3-031-58723-8_9'
apa: 'Tairi, E., & Ünal, A. (2024). Lower bounds for lattice-based compact functional
encryption. In Advances in Cryptology – EUROCRYPT 2024 (Vol. 14652, pp.
249–279). Zurich, Switzerland: Springer Nature. https://doi.org/10.1007/978-3-031-58723-8_9'
chicago: Tairi, Erkan, and Akin Ünal. “Lower Bounds for Lattice-Based Compact Functional
Encryption.” In Advances in Cryptology – EUROCRYPT 2024, 14652:249–79.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-58723-8_9.
ieee: E. Tairi and A. Ünal, “Lower bounds for lattice-based compact functional encryption,”
in Advances in Cryptology – EUROCRYPT 2024, Zurich, Switzerland, 2024,
vol. 14652, pp. 249–279.
ista: 'Tairi E, Ünal A. 2024. Lower bounds for lattice-based compact functional
encryption. Advances in Cryptology – EUROCRYPT 2024. EUROCRYPT: Theory and Applications
of Cryptographic Techniques, LNCS, vol. 14652, 249–279.'
mla: Tairi, Erkan, and Akin Ünal. “Lower Bounds for Lattice-Based Compact Functional
Encryption.” Advances in Cryptology – EUROCRYPT 2024, vol. 14652, Springer
Nature, 2024, pp. 249–79, doi:10.1007/978-3-031-58723-8_9.
short: E. Tairi, A. Ünal, in:, Advances in Cryptology – EUROCRYPT 2024, Springer
Nature, 2024, pp. 249–279.
conference:
end_date: 2024-05-30
location: Zurich, Switzerland
name: 'EUROCRYPT: Theory and Applications of Cryptographic Techniques'
start_date: 2024-05-26
date_created: 2024-06-09T22:01:03Z
date_published: 2024-05-08T00:00:00Z
date_updated: 2025-09-08T07:48:18Z
day: '08'
department:
- _id: KrPi
doi: 10.1007/978-3-031-58723-8_9
external_id:
isi:
- '001278247600009'
intvolume: ' 14652'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2023/719.pdf
month: '05'
oa: 1
oa_version: Submitted Version
page: 249-279
publication: Advances in Cryptology – EUROCRYPT 2024
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031587221'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Lower bounds for lattice-based compact functional encryption
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14652
year: '2024'
...
---
APC_amount: 2748 EUR
OA_place: publisher
OA_type: hybrid
_id: '18521'
abstract:
- lang: eng
text: In distributed systems with processes that do not share a global clock, partial
synchrony is achieved by clock synchronization that guarantees bounded clock skew
among all applications. Existing solutions for distributed runtime verification
under partial synchrony against temporal logic specifications are exact but suffer
from significant computational overhead. In this paper, we propose an approximate
distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates
this issue by abstracting away potential interleaving behaviors. This conservative
abstraction enables a significant speedup of the distributed monitors, albeit
with a tradeoff in accuracy. We address this tradeoff with a methodology that
combines our approximate monitor with its exact counterpart, resulting in enhanced
efficiency without sacrificing precision. We evaluate our approach with multiple
experiments, showcasing its efficacy in both real-world applications and synthetic
examples.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. This
work is sponsored in part by the United States NSF CCF-2118356 award. This research
was partially funded by A-IQ Ready (Chips JU, grant agreement No. 101096658).
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Borzoo
full_name: Bonakdarpour, Borzoo
last_name: Bonakdarpour
- first_name: Anik
full_name: Momtaz, Anik
last_name: Momtaz
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. Approximate distributed monitoring
under partial synchrony: Balancing speed & accuracy. In: 24th International
Conference on Runtime Verification. Vol 15191. Springer Nature; 2024:282-301.
doi:10.1007/978-3-031-74234-7_18'
apa: 'Bonakdarpour, B., Momtaz, A., Nickovic, D., & Sarac, N. E. (2024). Approximate
distributed monitoring under partial synchrony: Balancing speed & accuracy.
In 24th International Conference on Runtime Verification (Vol. 15191, pp.
282–301). Istanbul, Turkey: Springer Nature. https://doi.org/10.1007/978-3-031-74234-7_18'
chicago: 'Bonakdarpour, Borzoo, Anik Momtaz, Dejan Nickovic, and Naci E Sarac. “Approximate
Distributed Monitoring under Partial Synchrony: Balancing Speed & Accuracy.”
In 24th International Conference on Runtime Verification, 15191:282–301.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-74234-7_18.'
ieee: 'B. Bonakdarpour, A. Momtaz, D. Nickovic, and N. E. Sarac, “Approximate distributed
monitoring under partial synchrony: Balancing speed & accuracy,” in 24th
International Conference on Runtime Verification, Istanbul, Turkey, 2024,
vol. 15191, pp. 282–301.'
ista: 'Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. 2024. Approximate distributed
monitoring under partial synchrony: Balancing speed & accuracy. 24th International
Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS,
vol. 15191, 282–301.'
mla: 'Bonakdarpour, Borzoo, et al. “Approximate Distributed Monitoring under Partial
Synchrony: Balancing Speed & Accuracy.” 24th International Conference on
Runtime Verification, vol. 15191, Springer Nature, 2024, pp. 282–301, doi:10.1007/978-3-031-74234-7_18.'
short: B. Bonakdarpour, A. Momtaz, D. Nickovic, N.E. Sarac, in:, 24th International
Conference on Runtime Verification, Springer Nature, 2024, pp. 282–301.
conference:
end_date: 2024-10-17
location: Istanbul, Turkey
name: 'RV: Conference on Runtime Verification'
start_date: 2024-10-15
corr_author: '1'
date_created: 2024-11-10T23:01:58Z
date_published: 2024-10-12T00:00:00Z
date_updated: 2026-05-20T08:43:20Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
- _id: GradSch
doi: 10.1007/978-3-031-74234-7_18
ec_funded: 1
external_id:
arxiv:
- '2408.05033'
isi:
- '001420093700018'
file:
- access_level: open_access
checksum: 7b8ca21b8c19ab796fa445b0e54003ca
content_type: application/pdf
creator: dernst
date_created: 2024-11-11T09:42:28Z
date_updated: 2024-11-11T09:42:28Z
file_id: '18539'
file_name: 2024_LNCS_Bonakdarpour.pdf
file_size: 1897101
relation: main_file
success: 1
file_date_updated: 2024-11-11T09:42:28Z
has_accepted_license: '1'
intvolume: ' 15191'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 282-301
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 24th International Conference on Runtime Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031742330'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Approximate distributed monitoring under partial synchrony: Balancing speed
& accuracy'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15191
year: '2024'
...
---
OA_type: closed access
_id: '18563'
abstract:
- lang: eng
text: I give a personal account about the wave of new research activities that rose
in the 1990s on the specification, verification, and control of real-time systems.
acknowledgement: I thank all my collaborators over the years. None of the mentioned
contributions would have been possible without them. I also apologize for all omissions.
The selection of contributions in this essay reflects primarily my personal involvement
rather than any measure of importance.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Henzinger TA. Reminiscences of a Real-Time Researcher. In: Graf S, Pettersson
P, Steffen B, eds. Real Time and Such. Vol 15230. LNCS. Cham: Springer
Nature; 2024:154-164. doi:10.1007/978-3-031-73751-0_12'
apa: 'Henzinger, T. A. (2024). Reminiscences of a Real-Time Researcher. In S. Graf,
P. Pettersson, & B. Steffen (Eds.), Real Time and Such (Vol. 15230,
pp. 154–164). Cham: Springer Nature. https://doi.org/10.1007/978-3-031-73751-0_12'
chicago: 'Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” In Real
Time and Such, edited by Susanne Graf, Paul Pettersson, and Bernhard Steffen,
15230:154–64. LNCS. Cham: Springer Nature, 2024. https://doi.org/10.1007/978-3-031-73751-0_12.'
ieee: 'T. A. Henzinger, “Reminiscences of a Real-Time Researcher,” in Real Time
and Such, vol. 15230, S. Graf, P. Pettersson, and B. Steffen, Eds. Cham: Springer
Nature, 2024, pp. 154–164.'
ista: 'Henzinger TA. 2024.Reminiscences of a Real-Time Researcher. In: Real Time
and Such. LNCS, vol. 15230, 154–164.'
mla: Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” Real Time
and Such, edited by Susanne Graf et al., vol. 15230, Springer Nature, 2024,
pp. 154–64, doi:10.1007/978-3-031-73751-0_12.
short: T.A. Henzinger, in:, S. Graf, P. Pettersson, B. Steffen (Eds.), Real Time
and Such, Springer Nature, Cham, 2024, pp. 154–164.
corr_author: '1'
date_created: 2024-11-18T09:10:06Z
date_published: 2024-10-23T00:00:00Z
date_updated: 2025-08-05T12:19:50Z
day: '23'
department:
- _id: ToHe
doi: 10.1007/978-3-031-73751-0_12
editor:
- first_name: Susanne
full_name: Graf, Susanne
last_name: Graf
- first_name: Paul
full_name: Pettersson, Paul
last_name: Pettersson
- first_name: Bernhard
full_name: Steffen, Bernhard
last_name: Steffen
intvolume: ' 15230'
language:
- iso: eng
month: '10'
oa_version: None
page: 154-164
place: Cham
publication: Real Time and Such
publication_identifier:
eisbn:
- '9783031737510'
eissn:
- 1611-3349
isbn:
- '9783031737503'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Reminiscences of a Real-Time Researcher
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15230
year: '2024'
...
---
OA_type: closed access
_id: '18599'
abstract:
- lang: eng
text: "Hypernode logic can reason about the prefix relation on stutter-reduced finite
traces through the stutter-reduced prefix predicate. We increase the expressiveness
of hypernode logic in two ways. First, we split the stutter-reduced prefix predicate
into an explicit stutter-reduction operator and the classical prefix predicate
on words. This change gives hypernode logic the ability to combine synchronous
and asynchronous reasoning by explicitly stating which parts of traces can stutter.
Second, we allow the use of regular expressions in formulas to reason about the
structure of traces. This change enables hypernode logic to describe a mixture
of trace properties and hyperproperties.\r\n\r\nWe show how to translate extended
hypernode logic formulas into multi-track automata, which are automata that read
multiple input words. Then we describe a fully online monitoring algorithm for
monitoring k-safety hyperproperties specified in the logic. We have implemented
the monitoring algorithm, and evaluated it on monitoring synchronous and asynchronous
versions of observational determinism, and on checking the privacy preservation
by compiler optimizations."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, and
by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: 'Chalupa M, Henzinger TA, Oliveira da Costa A. Monitoring extended hypernode
logic. In: Integrated Formal Methods. Vol 15234. Springer Nature; 2024:151-171.
doi:10.1007/978-3-031-76554-4_9'
apa: Chalupa, M., Henzinger, T. A., & Oliveira da Costa, A. (2024). Monitoring
extended hypernode logic. In Integrated Formal Methods (Vol. 15234, pp.
151–171). Springer Nature. https://doi.org/10.1007/978-3-031-76554-4_9
chicago: Chalupa, Marek, Thomas A Henzinger, and Ana Oliveira da Costa. “Monitoring
Extended Hypernode Logic.” In Integrated Formal Methods, 15234:151–71.
Springer Nature, 2024. https://doi.org/10.1007/978-3-031-76554-4_9.
ieee: M. Chalupa, T. A. Henzinger, and A. Oliveira da Costa, “Monitoring extended
hypernode logic,” in Integrated Formal Methods, 2024, vol. 15234, pp. 151–171.
ista: Chalupa M, Henzinger TA, Oliveira da Costa A. 2024. Monitoring extended hypernode
logic. Integrated Formal Methods. , LNCS, vol. 15234, 151–171.
mla: Chalupa, Marek, et al. “Monitoring Extended Hypernode Logic.” Integrated
Formal Methods, vol. 15234, Springer Nature, 2024, pp. 151–71, doi:10.1007/978-3-031-76554-4_9.
short: M. Chalupa, T.A. Henzinger, A. Oliveira da Costa, in:, Integrated Formal
Methods, Springer Nature, 2024, pp. 151–171.
corr_author: '1'
date_created: 2024-12-01T23:01:52Z
date_published: 2024-11-13T00:00:00Z
date_updated: 2025-09-08T14:47:22Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-031-76554-4_9
ec_funded: 1
external_id:
isi:
- '001416640500009'
intvolume: ' 15234'
isi: 1
language:
- iso: eng
month: '11'
oa_version: None
page: 151-171
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Integrated Formal Methods
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031765537'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring extended hypernode logic
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15234
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '18600'
abstract:
- lang: eng
text: 'The analysis of formal models that include quantitative aspects such as timing
or probabilistic choices is performed by quantitative verification tools. Broad
and mature tool support is available for computing basic properties such as expected
rewards on basic models such as Markov chains. Previous editions of QComp, the
comparison of tools for the analysis of quantitative formal models, focused on
this setting. Many application scenarios, however, require more advanced property
types such as LTL and parameter synthesis queries as well as advanced models like
stochastic games and partially observable MDPs. For these, tool support is in
its infancy today. This paper presents the outcomes of QComp 2023: a survey of
the state of the art in quantitative verification tool support for advanced property
types and models. With tools ranging from first research prototypes to well-supported
integrations into established toolsets, this report highlights today’s active
areas and tomorrow’s challenges in tool-focused research for quantitative verification.'
acknowledgement: The authors are ordered alphabetically. This work was supported by
DFG RTG 2236/2 (UnRAVeL) and DFG project TRR 248 (CPEC, ID 389792660), by the EU
under MSCA grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199
(ProSVED), by ERC Starting Grant 101077178 (DEUCE), ERC Consolidator Grant 864075
(CAESAR), and ERC Advanced Grant 834115 (FUN2MODEL), by GAČR grant GA23-06963S (VESCAA),
by National Science Foundation grant 1856733, by NextGenerationEU project D53D23008400006
(SMARTITUDE), and by NWO VENI grant 639.021.754.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Roman
full_name: Andriushchenko, Roman
last_name: Andriushchenko
- first_name: Alexander
full_name: Bork, Alexander
last_name: Bork
- first_name: Carlos E.
full_name: Budde, Carlos E.
last_name: Budde
- first_name: Milan
full_name: Češka, Milan
last_name: Češka
- first_name: Kush
full_name: Grover, Kush
last_name: Grover
- first_name: Ernst Moritz
full_name: Hahn, Ernst Moritz
last_name: Hahn
- first_name: Arnd
full_name: Hartmanns, Arnd
last_name: Hartmanns
- first_name: Bryant
full_name: Israelsen, Bryant
last_name: Israelsen
- first_name: Nils
full_name: Jansen, Nils
last_name: Jansen
- first_name: Joshua
full_name: Jeppson, Joshua
last_name: Jeppson
- first_name: Sebastian
full_name: Junges, Sebastian
last_name: Junges
- first_name: Maximilian A.
full_name: Köhl, Maximilian A.
last_name: Köhl
- first_name: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: David
full_name: Parker, David
last_name: Parker
- first_name: Stefan
full_name: Pranger, Stefan
last_name: Pranger
- first_name: Tim
full_name: Quatmann, Tim
last_name: Quatmann
- first_name: Enno
full_name: Ruijters, Enno
last_name: Ruijters
- first_name: Landon
full_name: Taylor, Landon
last_name: Taylor
- first_name: Matthias
full_name: Volk, Matthias
last_name: Volk
- first_name: Maximilian
full_name: Weininger, Maximilian
id: 02ab0197-cc70-11ed-ab61-918e71f56881
last_name: Weininger
- first_name: Zhen
full_name: Zhang, Zhen
last_name: Zhang
citation:
ama: 'Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report. In: TOOLympics Challenge 2023.
Vol 14550. Springer Nature; 2024:90-146. doi:10.1007/978-3-031-67695-6_4'
apa: 'Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E.
M., … Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification: QComp
2023 Competition Report. In TOOLympics Challenge 2023 (Vol. 14550, pp.
90–146). Springer Nature. https://doi.org/10.1007/978-3-031-67695-6_4'
chicago: 'Andriushchenko, Roman, Alexander Bork, Carlos E. Budde, Milan Češka, Kush
Grover, Ernst Moritz Hahn, Arnd Hartmanns, et al. “Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report.” In TOOLympics Challenge 2023,
14550:90–146. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-67695-6_4.'
ieee: 'R. Andriushchenko et al., “Tools at the Frontiers of Quantitative
Verification: QComp 2023 Competition Report,” in TOOLympics Challenge 2023,
2024, vol. 14550, pp. 90–146.'
ista: 'Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM, Hartmanns
A, Israelsen B, Jansen N, Jeppson J, Junges S, Köhl MA, Könighofer B, Kretinsky
J, Meggendorfer T, Parker D, Pranger S, Quatmann T, Ruijters E, Taylor L, Volk
M, Weininger M, Zhang Z. 2024. Tools at the Frontiers of Quantitative Verification:
QComp 2023 Competition Report. TOOLympics Challenge 2023. , LNCS, vol. 14550,
90–146.'
mla: 'Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification:
QComp 2023 Competition Report.” TOOLympics Challenge 2023, vol. 14550,
Springer Nature, 2024, pp. 90–146, doi:10.1007/978-3-031-67695-6_4.'
short: R. Andriushchenko, A. Bork, C.E. Budde, M. Češka, K. Grover, E.M. Hahn, A.
Hartmanns, B. Israelsen, N. Jansen, J. Jeppson, S. Junges, M.A. Köhl, B. Könighofer,
J. Kretinsky, T. Meggendorfer, D. Parker, S. Pranger, T. Quatmann, E. Ruijters,
L. Taylor, M. Volk, M. Weininger, Z. Zhang, in:, TOOLympics Challenge 2023, Springer
Nature, 2024, pp. 90–146.
date_created: 2024-12-01T23:01:53Z
date_published: 2024-11-01T00:00:00Z
date_updated: 2025-09-08T14:45:11Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-031-67695-6_4
external_id:
arxiv:
- '2405.13583'
isi:
- '001434957500004'
intvolume: ' 14550'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.2405.13583'
month: '11'
oa: 1
oa_version: Preprint
page: 90-146
publication: TOOLympics Challenge 2023
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031676949'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition
Report'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14550
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '18702'
abstract:
- lang: eng
text: 'In this work we prove lower bounds on the (communication) cost of maintaining
a shared key among a dynamic group of users. Being “dynamic” means one can add
and remove users from the group. This captures important protocols like multicast
encryption (ME) and continuous group-key agreement (CGKA), which is the primitive
underlying many group messaging applications. We prove our bounds in a combinatorial
setting where the state of the protocol progresses in rounds. The state of the
protocol in each round is captured by a set system, with each of its elements
specifying a set of users who share a secret key. We show this combinatorial model
implies bounds in symbolic models for ME and CGKA that capture, as building blocks,
PRGs, PRFs, dual PRFs, secret sharing, and symmetric encryption in the setting
of ME, and PRGs, PRFs, dual PRFs, secret sharing, public-key encryption, and key-updatable
public-key encryption in the setting of CGKA. The models are related to the ones
used by Micciancio and Panjwani (Eurocrypt’04) and Bienstock et al. (TCC’20) to
analyze ME and CGKA, respectively. We prove – using the Bollobás’ Set Pairs Inequality
– that the cost (number of uploaded ciphertexts) for replacing a set of d users
in a group of size n is Ω(dln(n/d)). Our lower bound is asymptotically tight and
both improves on a bound of Ω(d) by Bienstock et al. (TCC’20), and generalizes
a result by Micciancio and Panjwani (Eurocrypt’04), who proved a lower bound of
Ω(log(n)) for d=1. '
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Michael
full_name: Anastos, Michael
id: 0b2a4358-bb35-11ec-b7b9-e3279b593dbb
last_name: Anastos
- first_name: Benedikt
full_name: Auerbach, Benedikt
id: D33D2B18-E445-11E9-ABB7-15F4E5697425
last_name: Auerbach
orcid: 0000-0002-7553-6606
- first_name: Mirza Ahad
full_name: Baig, Mirza Ahad
id: 3EDE6DE4-AA5A-11E9-986D-341CE6697425
last_name: Baig
- 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: Matthew Alan
full_name: Kwan, Matthew Alan
id: 5fca0887-a1db-11eb-95d1-ca9d5e0453b3
last_name: Kwan
orcid: 0000-0002-4003-7567
- first_name: Guillermo
full_name: Pascual Perez, Guillermo
id: 2D7ABD02-F248-11E8-B48F-1D18A9856A87
last_name: Pascual Perez
orcid: 0000-0001-8630-415X
- 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: 'Anastos M, Auerbach B, Baig MA, et al. The cost of maintaining keys in dynamic
groups with applications to multicast encryption and group messaging. In: 22nd
International Conference on Theory of Cryptography. Vol 15364. Springer Nature;
2024:413-443. doi:10.1007/978-3-031-78011-0_14'
apa: 'Anastos, M., Auerbach, B., Baig, M. A., Cueto Noval, M., Kwan, M. A., Pascual
Perez, G., & Pietrzak, K. Z. (2024). The cost of maintaining keys in dynamic
groups with applications to multicast encryption and group messaging. In 22nd
International Conference on Theory of Cryptography (Vol. 15364, pp. 413–443).
Milan, Italy: Springer Nature. https://doi.org/10.1007/978-3-031-78011-0_14'
chicago: Anastos, Michael, Benedikt Auerbach, Mirza Ahad Baig, Miguel Cueto Noval,
Matthew Alan Kwan, Guillermo Pascual Perez, and Krzysztof Z Pietrzak. “The Cost
of Maintaining Keys in Dynamic Groups with Applications to Multicast Encryption
and Group Messaging.” In 22nd International Conference on Theory of Cryptography,
15364:413–43. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-78011-0_14.
ieee: M. Anastos et al., “The cost of maintaining keys in dynamic groups
with applications to multicast encryption and group messaging,” in 22nd International
Conference on Theory of Cryptography, Milan, Italy, 2024, vol. 15364, pp.
413–443.
ista: 'Anastos M, Auerbach B, Baig MA, Cueto Noval M, Kwan MA, Pascual Perez G,
Pietrzak KZ. 2024. The cost of maintaining keys in dynamic groups with applications
to multicast encryption and group messaging. 22nd International Conference on
Theory of Cryptography. TCC: Theory of Cryptography, LNCS, vol. 15364, 413–443.'
mla: Anastos, Michael, et al. “The Cost of Maintaining Keys in Dynamic Groups with Applications
to Multicast Encryption and Group Messaging.” 22nd International Conference
on Theory of Cryptography, vol. 15364, Springer Nature, 2024, pp. 413–43,
doi:10.1007/978-3-031-78011-0_14.
short: M. Anastos, B. Auerbach, M.A. Baig, M. Cueto Noval, M.A. Kwan, G. Pascual
Perez, K.Z. Pietrzak, in:, 22nd International Conference on Theory of Cryptography,
Springer Nature, 2024, pp. 413–443.
conference:
end_date: 2024-12-06
location: Milan, Italy
name: 'TCC: Theory of Cryptography'
start_date: 2024-12-02
corr_author: '1'
date_created: 2024-12-22T23:01:47Z
date_published: 2024-12-02T00:00:00Z
date_updated: 2025-12-02T13:55:46Z
day: '02'
department:
- _id: MaKw
- _id: KrPi
doi: 10.1007/978-3-031-78011-0_14
external_id:
isi:
- '001545628900014'
intvolume: ' 15364'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2024/1097
month: '12'
oa: 1
oa_version: Preprint
page: 413-443
publication: 22nd International Conference on Theory of Cryptography
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031780103'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: The cost of maintaining keys in dynamic groups with applications to multicast
encryption and group messaging
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15364
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '18755'
abstract:
- lang: eng
text: "A universalthresholdizer (UT), constructed from a threshold fully homomorphic
encryption by Boneh et. al , Crypto 2018, is a general framework for universally
thresholdizing many cryptographic schemes. However, their framework is insufficient
to construct strongly secure threshold schemes, such as threshold signatures and
threshold public-key encryption, etc.\r\n\r\nIn this paper, we strengthen the
security definition for a universal thresholdizer and propose a scheme which satisfies
our stronger security notion. Our UT scheme is an improvement of Boneh et. al
’s construction at the level of threshold fully homomorphic encryption using a
key homomorphic pseudorandom function. We apply our strongly secure UT scheme
to construct strongly secure threshold signatures and threshold public-key encryption."
acknowledgement: Ehsan Ebrahimi is supported by the Luxembourg National Research Fund
under the Junior CORE project QSP (C22/IS/17272217/QSP/Ebrahimi).
article_processing_charge: No
author:
- first_name: Ehsan
full_name: Ebrahimi, Ehsan
last_name: Ebrahimi
- first_name: Anshu
full_name: Yadav, Anshu
id: dc8f1524-403e-11ee-bf07-9649ad996e21
last_name: Yadav
citation:
ama: 'Ebrahimi E, Yadav A. Strongly secure universal thresholdizer. In: 30th
International Conference on the Theory and Application of Cryptology and Information
Security. Vol 15486. Springer Nature; 2024:207-239. doi:10.1007/978-981-96-0891-1_7'
apa: 'Ebrahimi, E., & Yadav, A. (2024). Strongly secure universal thresholdizer.
In 30th International Conference on the Theory and Application of Cryptology
and Information Security (Vol. 15486, pp. 207–239). Kolkata, India: Springer
Nature. https://doi.org/10.1007/978-981-96-0891-1_7'
chicago: Ebrahimi, Ehsan, and Anshu Yadav. “Strongly Secure Universal Thresholdizer.”
In 30th International Conference on the Theory and Application of Cryptology
and Information Security, 15486:207–39. Springer Nature, 2024. https://doi.org/10.1007/978-981-96-0891-1_7.
ieee: E. Ebrahimi and A. Yadav, “Strongly secure universal thresholdizer,” in 30th
International Conference on the Theory and Application of Cryptology and Information
Security, Kolkata, India, 2024, vol. 15486, pp. 207–239.
ista: 'Ebrahimi E, Yadav A. 2024. Strongly secure universal thresholdizer. 30th
International Conference on the Theory and Application of Cryptology and Information
Security. ASIACRYPT: Conference on the Theory and Application of Cryptology and
Information Security vol. 15486, 207–239.'
mla: Ebrahimi, Ehsan, and Anshu Yadav. “Strongly Secure Universal Thresholdizer.”
30th International Conference on the Theory and Application of Cryptology and
Information Security, vol. 15486, Springer Nature, 2024, pp. 207–39, doi:10.1007/978-981-96-0891-1_7.
short: E. Ebrahimi, A. Yadav, in:, 30th International Conference on the Theory and
Application of Cryptology and Information Security, Springer Nature, 2024, pp.
207–239.
conference:
end_date: 2024-12-13
location: Kolkata, India
name: 'ASIACRYPT: Conference on the Theory and Application of Cryptology and Information
Security'
start_date: 2024-12-09
date_created: 2025-01-05T23:01:56Z
date_published: 2024-12-12T00:00:00Z
date_updated: 2025-09-09T12:00:12Z
day: '12'
department:
- _id: KrPi
doi: 10.1007/978-981-96-0891-1_7
external_id:
isi:
- '001443889100007'
intvolume: ' 15486'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2024/2078
month: '12'
oa: 1
oa_version: Preprint
page: 207-239
publication: 30th International Conference on the Theory and Application of Cryptology
and Information Security
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9789819608904'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Strongly secure universal thresholdizer
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15486
year: '2024'
...
---
OA_place: repository
OA_type: green
_id: '18756'
abstract:
- lang: eng
text: "The evasive LWE assumption, proposed by Wee [Eurocrypt’22 Wee] for constructing
a lattice-based optimal broadcast encryption, has shown to be a powerful assumption,
adopted by subsequent works to construct advanced primitives ranging from ABE
variants to obfuscation for null circuits. However, a closer look reveals significant
differences among the precise assumption statements involved in different works,
leading to the fundamental question of how these assumptions compare to each other.
In this work, we initiate a more systematic study on evasive LWE assumptions:\r\n(i)
Based on the standard LWE assumption, we construct simple counterexamples against
three private-coin evasive LWE variants, used in [Crypto’22 Tsabary, Asiacrypt’22
VWW, Crypto’23 ARYY] respectively, showing that these assumptions are unlikely
to hold.\r\n\r\n(ii) Based on existing evasive LWE variants and our counterexamples,
we propose and define three classes of plausible evasive LWE assumptions, suitably
capturing all existing variants for which we are not aware of non-obfuscation-based
counterexamples.\r\n\r\n(iii) We show that under our assumption formulations,
the security proofs of [Asiacrypt’22 VWW] and [Crypto’23 ARYY] can be recovered,
and we reason why the security proof of [Crypto’22 Tsabary] is also plausibly
repairable using an appropriate evasive LWE assumption."
acknowledgement: The authors thank the anonymous reviewers for insightful comments
which very much improved this work, in particular, sharing with us the counterexamples
against a prior version of Hiding Evasive LWE, and against public-coin Evasive LWE
when the sampler inputs B. Chris Brzuska and Ivy K. Y. Woo are supported by Research
Council of Finland grant 358950. We thank Russell W. F. Lai and Hoeteck Wee for
helpful discussions.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Chris
full_name: Brzuska, Chris
last_name: Brzuska
- first_name: Akin
full_name: Ünal, Akin
id: f6b56fb6-dc63-11ee-9dbf-f6780863a85a
last_name: Ünal
orcid: 0000-0002-8929-0221
- first_name: Ivy K.Y.
full_name: Woo, Ivy K.Y.
last_name: Woo
citation:
ama: 'Brzuska C, Ünal A, Woo IKY. Evasive LWE assumptions: Definitions, classes,
and counterexamples. In: 30th International Conference on the Theory and Application
of Cryptology and Information Security. Vol 15487. Springer Nature; 2024:418-449.
doi:10.1007/978-981-96-0894-2_14'
apa: 'Brzuska, C., Ünal, A., & Woo, I. K. Y. (2024). Evasive LWE assumptions:
Definitions, classes, and counterexamples. In 30th International Conference
on the Theory and Application of Cryptology and Information Security (Vol.
15487, pp. 418–449). Kolkata, India: Springer Nature. https://doi.org/10.1007/978-981-96-0894-2_14'
chicago: 'Brzuska, Chris, Akin Ünal, and Ivy K.Y. Woo. “Evasive LWE Assumptions:
Definitions, Classes, and Counterexamples.” In 30th International Conference
on the Theory and Application of Cryptology and Information Security, 15487:418–49.
Springer Nature, 2024. https://doi.org/10.1007/978-981-96-0894-2_14.'
ieee: 'C. Brzuska, A. Ünal, and I. K. Y. Woo, “Evasive LWE assumptions: Definitions,
classes, and counterexamples,” in 30th International Conference on the Theory
and Application of Cryptology and Information Security, Kolkata, India, 2024,
vol. 15487, pp. 418–449.'
ista: 'Brzuska C, Ünal A, Woo IKY. 2024. Evasive LWE assumptions: Definitions, classes,
and counterexamples. 30th International Conference on the Theory and Application
of Cryptology and Information Security. ASIACRYPT: Conference on the Theory and
Application of Cryptology and Information Security, LNCS, vol. 15487, 418–449.'
mla: 'Brzuska, Chris, et al. “Evasive LWE Assumptions: Definitions, Classes, and Counterexamples.”
30th International Conference on the Theory and Application of Cryptology and
Information Security, vol. 15487, Springer Nature, 2024, pp. 418–49, doi:10.1007/978-981-96-0894-2_14.'
short: C. Brzuska, A. Ünal, I.K.Y. Woo, in:, 30th International Conference on the
Theory and Application of Cryptology and Information Security, Springer Nature,
2024, pp. 418–449.
conference:
end_date: 2024-12-13
location: Kolkata, India
name: 'ASIACRYPT: Conference on the Theory and Application of Cryptology and Information
Security'
start_date: 2024-12-09
date_created: 2025-01-05T23:01:56Z
date_published: 2024-12-13T00:00:00Z
date_updated: 2025-09-09T12:00:51Z
day: '13'
department:
- _id: KrPi
doi: 10.1007/978-981-96-0894-2_14
external_id:
isi:
- '001443890800014'
intvolume: ' 15487'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2024/2000
month: '12'
oa: 1
oa_version: Preprint
page: 418-449
publication: 30th International Conference on the Theory and Application of Cryptology
and Information Security
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9789819608935'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Evasive LWE assumptions: Definitions, classes, and counterexamples'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15487
year: '2024'
...
---
_id: '17402'
abstract:
- lang: eng
text: We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification
of probabilistic systems. We extend the previous version by adding support for
stochastic games, based on a recent unified framework for sound value iteration
algorithms. Thereby, PET2 is the first tool implementing a sound and efficient
approach for solving stochastic games with objectives of the type reachability/safety
and mean payoff. We complement this approach by developing and implementing a
partial-exploration based variant for all three objectives. Our experimental evaluation
shows that PET2 offers the most efficient partial-exploration based algorithm
and is the most viable tool on SGs, even outperforming unsound tools.
acknowledgement: M. Weininger has received funding from the EU’s Horizon 2020 research
and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101034413.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
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
citation:
ama: 'Meggendorfer T, Weininger M. Playing games with your PET: Extending the Partial
Exploration Tool to stochastic games. In: 36th International Conference on
Computer Aided Verification. Vol 14683. Springer Nature; 2024:359-372. doi:10.1007/978-3-031-65633-0_16'
apa: 'Meggendorfer, T., & Weininger, M. (2024). Playing games with your PET:
Extending the Partial Exploration Tool to stochastic games. In 36th International
Conference on Computer Aided Verification (Vol. 14683, pp. 359–372). Montreal,
Canada: Springer Nature. https://doi.org/10.1007/978-3-031-65633-0_16'
chicago: 'Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your
PET: Extending the Partial Exploration Tool to Stochastic Games.” In 36th International
Conference on Computer Aided Verification, 14683:359–72. Springer Nature,
2024. https://doi.org/10.1007/978-3-031-65633-0_16.'
ieee: 'T. Meggendorfer and M. Weininger, “Playing games with your PET: Extending
the Partial Exploration Tool to stochastic games,” in 36th International Conference
on Computer Aided Verification, Montreal, Canada, 2024, vol. 14683, pp. 359–372.'
ista: 'Meggendorfer T, Weininger M. 2024. Playing games with your PET: Extending
the Partial Exploration Tool to stochastic games. 36th International Conference
on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 14683,
359–372.'
mla: 'Meggendorfer, Tobias, and Maximilian Weininger. “Playing Games with Your PET:
Extending the Partial Exploration Tool to Stochastic Games.” 36th International
Conference on Computer Aided Verification, vol. 14683, Springer Nature, 2024,
pp. 359–72, doi:10.1007/978-3-031-65633-0_16.'
short: T. Meggendorfer, M. Weininger, in:, 36th International Conference on Computer
Aided Verification, Springer Nature, 2024, pp. 359–372.
conference:
end_date: 2024-07-27
location: Montreal, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2024-07-24
corr_author: '1'
date_created: 2024-08-09T11:24:54Z
date_published: 2024-07-01T00:00:00Z
date_updated: 2025-09-08T08:53:55Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-65633-0_16
ec_funded: 1
external_id:
arxiv:
- '2405.03885'
isi:
- '001307897000016'
file:
- access_level: open_access
checksum: c888231d0a47b55786b7b4c0f02216bb
content_type: application/pdf
creator: dernst
date_created: 2024-08-12T08:39:12Z
date_updated: 2024-08-12T08:39:12Z
file_id: '17419'
file_name: 2024_CAV_Meggendorfer.pdf
file_size: 368487
relation: main_file
success: 1
file_date_updated: 2024-08-12T08:39:12Z
has_accepted_license: '1'
intvolume: ' 14683'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 359-372
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: 36th International Conference on Computer Aided Verification
publication_identifier:
eisbn:
- '9783031656330'
eissn:
- 1611-3349
isbn:
- '9783031656323'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Playing games with your PET: Extending the Partial Exploration Tool to stochastic
games'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14683
year: '2024'
...
---
_id: '17413'
abstract:
- lang: eng
text: Certification helps to increase trust in formal verification of safety-critical
systems which require assurance on their correctness. In hardware model checking,
a widely used formal verification technique, phase abstraction is considered one
of the most commonly used preprocessing techniques. We present an approach to
certify an extended form of phase abstraction using a generic certificate format.
As in earlier works our approach involves constructing a witness circuit with
an inductive invariant property that certifies the correctness of the entire model
checking process, which is then validated by an independent certificate checker.
We have implemented and evaluated the proposed approach including certification
for various preprocessing configurations on hardware model checking competition
benchmarks. As an improvement on previous work in this area, the proposed method
is able to efficiently complete certification with an overhead of a fraction of
model checking time.
acknowledgement: This work is supported by the Austrian Science Fund (FWF) under the
project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG
101020093, the Academy of Finland under the project 336092 and by a gift from Intel
Corporation.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Nils
full_name: Froleyks, Nils
last_name: Froleyks
- first_name: Zhengqi
full_name: Yu, Zhengqi
id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
last_name: Yu
- first_name: Armin
full_name: Biere, Armin
last_name: Biere
- first_name: Keijo
full_name: Heljanko, Keijo
last_name: Heljanko
citation:
ama: 'Froleyks N, Yu E, Biere A, Heljanko K. Certifying phase abstraction. In: Lecture
Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics). Vol 14739. Springer Nature; 2024:284-303.
doi:10.1007/978-3-031-63498-7_17'
apa: 'Froleyks, N., Yu, E., Biere, A., & Heljanko, K. (2024). Certifying phase
abstraction. In Lecture Notes in Computer Science (including subseries Lecture
Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol.
14739, pp. 284–303). Nancy, France: Springer Nature. https://doi.org/10.1007/978-3-031-63498-7_17'
chicago: Froleyks, Nils, Emily Yu, Armin Biere, and Keijo Heljanko. “Certifying
Phase Abstraction.” In Lecture Notes in Computer Science (Including Subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
14739:284–303. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-63498-7_17.
ieee: N. Froleyks, E. Yu, A. Biere, and K. Heljanko, “Certifying phase abstraction,”
in Lecture Notes in Computer Science (including subseries Lecture Notes in
Artificial Intelligence and Lecture Notes in Bioinformatics), Nancy, France,
2024, vol. 14739, pp. 284–303.
ista: 'Froleyks N, Yu E, Biere A, Heljanko K. 2024. Certifying phase abstraction.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics). IJCAR: International Joint
Conference on Automated Reasoning, LNCS, vol. 14739, 284–303.'
mla: Froleyks, Nils, et al. “Certifying Phase Abstraction.” Lecture Notes in
Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
and Lecture Notes in Bioinformatics), vol. 14739, Springer Nature, 2024, pp.
284–303, doi:10.1007/978-3-031-63498-7_17.
short: N. Froleyks, E. Yu, A. Biere, K. Heljanko, in:, Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics), Springer Nature, 2024, pp. 284–303.
conference:
end_date: 2024-07-06
location: Nancy, France
name: 'IJCAR: International Joint Conference on Automated Reasoning'
start_date: 2024-07-03
date_created: 2024-08-11T22:01:13Z
date_published: 2024-07-01T00:00:00Z
date_updated: 2025-09-08T08:49:53Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-63498-7_17
ec_funded: 1
external_id:
arxiv:
- '2405.04297'
isi:
- '001273489700017'
file:
- access_level: open_access
checksum: 7d7839fc8c5c680ea3ac09f40a66e55d
content_type: application/pdf
creator: dernst
date_created: 2024-08-12T06:53:39Z
date_updated: 2024-08-12T06:53:39Z
file_id: '17414'
file_name: 2024_LNCS_Froleyks.pdf
file_size: 556902
relation: main_file
success: 1
file_date_updated: 2024-08-12T06:53:39Z
has_accepted_license: '1'
intvolume: ' 14739'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 284-303
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031634970'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Certifying phase abstraction
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14739
year: '2024'
...
---
APC_amount: 2748 EUR
OA_place: publisher
OA_type: hybrid
_id: '17634'
abstract:
- lang: eng
text: System behaviors are traditionally evaluated through binary classifications
of correctness, which do not suffice for properties involving quantitative aspects
of systems and executions. Quantitative automata offer a more nuanced approach,
mapping each execution to a real number by incorporating weighted transitions
and value functions generalizing acceptance conditions. In this paper, we introduce
QuAK, the first tool designed to automate the analysis of quantitative automata.
QuAK currently supports a variety of quantitative automaton types, including Inf,
Sup, LimInf, LimSup, LimInfAvg, and LimSupAvg automata, and implements decision
procedures for problems such as emptiness, universality, inclusion, equivalence,
as well as for checking whether an automaton is safe, live, or constant. Additionally,
QuAK is able to compute extremal values when possible, construct safety-liveness
decompositions, and monitor system behaviors. We demonstrate the effectiveness
of QuAK through experiments focusing on the inclusion, constant-function check,
and monitoring problems.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. N.
Mazzocchi was affiliated with ISTA when his collaboration started.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
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. QuAK: Quantitative Automata
Kit. In: 12th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation. Vol 15222. Springer Nature; 2024:3-20.
doi:10.1007/978-3-031-75387-9_1'
apa: 'Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2024).
QuAK: Quantitative Automata Kit. In 12th International Symposium on Leveraging
Applications of Formal Methods, Verification and Validation (Vol. 15222, pp.
3–20). Crete, Greece: Springer Nature. https://doi.org/10.1007/978-3-031-75387-9_1'
chicago: 'Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci
E Sarac. “QuAK: Quantitative Automata Kit.” In 12th International Symposium
on Leveraging Applications of Formal Methods, Verification and Validation,
15222:3–20. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-75387-9_1.'
ieee: 'M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “QuAK: Quantitative
Automata Kit,” in 12th International Symposium on Leveraging Applications of
Formal Methods, Verification and Validation, Crete, Greece, 2024, vol. 15222,
pp. 3–20.'
ista: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2024. QuAK: Quantitative
Automata Kit. 12th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation. ISoLA: International Symposium on Leveraging
Applications, LNCS, vol. 15222, 3–20.'
mla: 'Chalupa, Marek, et al. “QuAK: Quantitative Automata Kit.” 12th International
Symposium on Leveraging Applications of Formal Methods, Verification and Validation,
vol. 15222, Springer Nature, 2024, pp. 3–20, doi:10.1007/978-3-031-75387-9_1.'
short: M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 12th International
Symposium on Leveraging Applications of Formal Methods, Verification and Validation,
Springer Nature, 2024, pp. 3–20.
conference:
end_date: 2024-10-31
location: Crete, Greece
name: 'ISoLA: International Symposium on Leveraging Applications'
start_date: 2024-10-27
corr_author: '1'
date_created: 2024-09-05T14:27:08Z
date_published: 2024-10-26T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '26'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-75387-9_1
ec_funded: 1
external_id:
arxiv:
- '2409.03569'
isi:
- '001419008700001'
file:
- access_level: open_access
checksum: 43e432f82be376434b358f3dd7a94b71
content_type: application/pdf
creator: esarac
date_created: 2024-09-05T14:26:02Z
date_updated: 2024-09-05T14:26:02Z
file_id: '17635'
file_name: isola24.pdf
file_size: 847422
relation: main_file
success: 1
- access_level: open_access
checksum: 6bc04f07bb5612c0e7ea00ac121a69b6
content_type: application/pdf
creator: dernst
date_created: 2025-01-21T14:39:49Z
date_updated: 2025-01-21T14:39:49Z
file_id: '18865'
file_name: 2024_LNCS_Chalupa.pdf
file_size: 1358706
relation: main_file
success: 1
file_date_updated: 2025-01-21T14:39:49Z
has_accepted_license: '1'
intvolume: ' 15222'
isi: 1
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 3-20
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 12th International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031753862'
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: 'QuAK: Quantitative Automata Kit'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15222
year: '2024'
...
---
_id: '18086'
abstract:
- lang: eng
text: "Abstract. Continuous group key agreement (CGKA) allows a group of\r\nusers
to maintain a continuously updated shared key in an asynchronous\r\nsetting where
parties only come online sporadically and their messages\r\nare relayed by an
untrusted server. CGKA captures the basic primitive\r\nunderlying group messaging
schemes.\r\nCurrent solutions including TreeKEM (“Messaging Layer Security”\r\n(MLS)
IETF RFC 9420) cannot handle concurrent requests while retaining low communication
complexity. The exception being CoCoA, which\r\nis concurrent while having extremely
low communication complexity (in\r\ngroups of size n and for m concurrent updates
the communication per\r\nuser is log(n), i.e., independent of m). The main downside
of CoCoA\r\nis that in groups of size n, users might have to do up to log(n) update\r\nrequests
to the server to ensure their (potentially corrupted) key material has been refreshed.\r\nIn
this work we present a “fast healing” concurrent CGKA protocol,\r\nnamed DeCAF,
where users will heal after at most log(t) requests, with\r\nt being the number
of corrupted users. While also suitable for the standard central-server setting,
our protocol is particularly interesting for\r\nrealizing decentralized group
messaging, where protocol messages (add,\r\nremove, update) are being posted on
some append-only data structure\r\nrather than sent to a server. In this setting,
concurrency is crucial once\r\nthe rate of requests exceeds, say, the rate at
which new blocks are added\r\nto a blockchain.\r\nIn the central-server setting,
CoCoA (the only alternative with concurrency, sub-linear communication and basic
post-compromise security)\r\nenjoys much lower download communication. However,
in the decentralized setting – where there is no server which can craft specific
messages\r\nfor different users to reduce their download communication – our protocol\r\nsignificantly
outperforms CoCoA. DeCAF heals in fewer epochs (log(t)\r\nvs. log(n)) while incurring
a similar per epoch per user communication\r\ncost."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Joel F
full_name: Alwen, Joel F
id: 2A8DFA8C-F248-11E8-B48F-1D18A9856A87
last_name: Alwen
- 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: Karen
full_name: Klein, Karen
id: 3E83A2F8-F248-11E8-B48F-1D18A9856A87
last_name: Klein
- first_name: Guillermo
full_name: Pascual Perez, Guillermo
id: 2D7ABD02-F248-11E8-B48F-1D18A9856A87
last_name: Pascual Perez
orcid: 0000-0001-8630-415X
- 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: 'Alwen JF, Auerbach B, Cueto Noval M, Klein K, Pascual Perez G, Pietrzak KZ.
DeCAF: Decentralizable CGKA with fast healing. In: Galdi C, Phan DH, eds. Security
and Cryptography for Networks: 14th International Conference. Vol 14974. Cham:
Springer Nature; 2024:294–313. doi:10.1007/978-3-031-71073-5_14'
apa: 'Alwen, J. F., Auerbach, B., Cueto Noval, M., Klein, K., Pascual Perez, G.,
& Pietrzak, K. Z. (2024). DeCAF: Decentralizable CGKA with fast healing. In
C. Galdi & D. H. Phan (Eds.), Security and Cryptography for Networks: 14th
International Conference (Vol. 14974, pp. 294–313). Cham: Springer Nature.
https://doi.org/10.1007/978-3-031-71073-5_14'
chicago: 'Alwen, Joel F, Benedikt Auerbach, Miguel Cueto Noval, Karen Klein, Guillermo
Pascual Perez, and Krzysztof Z Pietrzak. “DeCAF: Decentralizable CGKA with Fast
Healing.” In Security and Cryptography for Networks: 14th International Conference,
edited by Clemente Galdi and Duong Hieu Phan, 14974:294–313. Cham: Springer Nature,
2024. https://doi.org/10.1007/978-3-031-71073-5_14.'
ieee: 'J. F. Alwen, B. Auerbach, M. Cueto Noval, K. Klein, G. Pascual Perez, and
K. Z. Pietrzak, “DeCAF: Decentralizable CGKA with fast healing,” in Security
and Cryptography for Networks: 14th International Conference, Amalfi, Italy,
2024, vol. 14974, pp. 294–313.'
ista: 'Alwen JF, Auerbach B, Cueto Noval M, Klein K, Pascual Perez G, Pietrzak KZ.
2024. DeCAF: Decentralizable CGKA with fast healing. Security and Cryptography
for Networks: 14th International Conference. SCN: Security and Cryptography for
Networks, LNCS, vol. 14974, 294–313.'
mla: 'Alwen, Joel F., et al. “DeCAF: Decentralizable CGKA with Fast Healing.” Security
and Cryptography for Networks: 14th International Conference, edited by Clemente
Galdi and Duong Hieu Phan, vol. 14974, Springer Nature, 2024, pp. 294–313, doi:10.1007/978-3-031-71073-5_14.'
short: 'J.F. Alwen, B. Auerbach, M. Cueto Noval, K. Klein, G. Pascual Perez, K.Z.
Pietrzak, in:, C. Galdi, D.H. Phan (Eds.), Security and Cryptography for Networks:
14th International Conference, Springer Nature, Cham, 2024, pp. 294–313.'
conference:
end_date: 2024-09-13
location: Amalfi, Italy
name: 'SCN: Security and Cryptography for Networks'
start_date: 2024-09-11
corr_author: '1'
date_created: 2024-09-18T11:35:14Z
date_published: 2024-09-10T00:00:00Z
date_updated: 2026-04-07T13:01:26Z
day: '10'
department:
- _id: GradSch
- _id: KrPi
doi: 10.1007/978-3-031-71073-5_14
editor:
- first_name: Clemente
full_name: Galdi, Clemente
last_name: Galdi
- first_name: Duong Hieu
full_name: Phan, Duong Hieu
last_name: Phan
external_id:
isi:
- '001330408000014'
intvolume: ' 14974'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 294–313
place: Cham
publication: 'Security and Cryptography for Networks: 14th International Conference'
publication_identifier:
eisbn:
- '9783031710735'
eissn:
- 1611-3349
isbn:
- '9783031710728'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '18088'
relation: dissertation_contains
status: public
status: public
title: 'DeCAF: Decentralizable CGKA with fast healing'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14974
year: '2024'
...
---
_id: '18155'
abstract:
- lang: eng
text: We study the classical problem of verifying programs with respect to formal
specifications given in the linear temporal logic (LTL). We first present novel
sound and complete witnesses for LTL verification over imperative programs. Our
witnesses are applicable to both verification (proving) and refutation (finding
bugs) settings. We then consider LTL formulas in which atomic propositions can
be polynomial constraints and turn our focus to polynomial arithmetic programs,
i.e. programs in which every assignment and guard consists only of polynomial
expressions. For this setting, we provide an efficient algorithm to automatically
synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete.
Finally, we present experimental results demonstrating the effectiveness of our
approach and that it can handle programs which were beyond the reach of previous
state-of-the-art tools.
acknowledgement: This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt)
and the Hong Kong Research Grants Council ECS Project Number 26208122.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
full_name: Goharshady, Amir Kafshdar
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Ehsan
full_name: Goharshady, Ehsan
last_name: Goharshady
- first_name: Mehrdad
full_name: Karrabi, Mehrdad
id: 67638922-f394-11eb-9cf6-f20423e08757
last_name: Karrabi
- first_name: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. Sound and complete
witnesses for template-based verification of LTL properties on polynomial programs.
In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in
Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 14933. Springer
Nature; 2024:600-619. doi:10.1007/978-3-031-71162-6_31'
apa: 'Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., & Zikelic,
D. (2024). Sound and complete witnesses for template-based verification of LTL
properties on polynomial programs. In Lecture Notes in Computer Science (including
subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
(Vol. 14933, pp. 600–619). Milan, Italy: Springer Nature. https://doi.org/10.1007/978-3-031-71162-6_31'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad
Karrabi, and Dorde Zikelic. “Sound and Complete Witnesses for Template-Based Verification
of LTL Properties on Polynomial Programs.” In Lecture Notes in Computer Science
(Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes
in Bioinformatics), 14933:600–619. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-71162-6_31.
ieee: K. Chatterjee, A. K. Goharshady, E. Goharshady, M. Karrabi, and D. Zikelic,
“Sound and complete witnesses for template-based verification of LTL properties
on polynomial programs,” in Lecture Notes in Computer Science (including subseries
Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),
Milan, Italy, 2024, vol. 14933, pp. 600–619.
ista: 'Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. 2024. Sound
and complete witnesses for template-based verification of LTL properties on polynomial
programs. Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics). FM: Formal Methods,
LNCS, vol. 14933, 600–619.'
mla: Chatterjee, Krishnendu, et al. “Sound and Complete Witnesses for Template-Based
Verification of LTL Properties on Polynomial Programs.” Lecture Notes in Computer
Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
Notes in Bioinformatics), vol. 14933, Springer Nature, 2024, pp. 600–19, doi:10.1007/978-3-031-71162-6_31.
short: K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, D. Zikelic, in:,
Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp.
600–619.
conference:
end_date: 2024-09-13
location: Milan, Italy
name: 'FM: Formal Methods'
start_date: 2024-09-09
corr_author: '1'
date_created: 2024-09-29T22:01:37Z
date_published: 2024-09-11T00:00:00Z
date_updated: 2025-09-08T09:51:34Z
day: '11'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-71162-6_31
ec_funded: 1
external_id:
arxiv:
- '2403.05386'
isi:
- '001336893300031'
file:
- access_level: open_access
checksum: 223845be9e754681ee218866827c95e7
content_type: application/pdf
creator: dernst
date_created: 2024-10-01T09:56:54Z
date_updated: 2024-10-01T09:56:54Z
file_id: '18165'
file_name: 2024_LNCS_Chatterjee.pdf
file_size: 650495
relation: main_file
success: 1
file_date_updated: 2024-10-01T09:56:54Z
has_accepted_license: '1'
intvolume: ' 14933'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 600-619
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031711619'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Sound and complete witnesses for template-based verification of LTL properties
on polynomial programs
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14933
year: '2024'
...
---
_id: '18177'
abstract:
- lang: eng
text: Partially Specified Boolean Networks (PSBNs) represent a family of Boolean
models resulting from possible interpretations of unknown update logics. Hybrid
extension of CTL (HCTL) has the power to express complex dynamical phenomena,
such as oscillations or stability. We present BNClassifier to classify Boolean
Networks corresponding to a given PSBN according to criteria specified in HCTL.
The implementation of the tool is fully symbolic (based on BDDs). The results
are visualised using the machine-learning-based technology of decision trees.
acknowledgement: The work has been supported by the Czech Science Foundation grant
No. GA22-10845S. This project has received funding from the European Union’s Horizon
2020 research and innovation programme under the Marie Sklodowska-Curie Grant Agreement
No. 101034413.
alternative_title:
- LNBI
article_processing_charge: No
author:
- first_name: Nikola
full_name: Beneš, Nikola
last_name: Beneš
- first_name: Luboš
full_name: Brim, Luboš
last_name: Brim
- first_name: Ondřej
full_name: Huvar, Ondřej
last_name: Huvar
- first_name: Samuel
full_name: Pastva, Samuel
id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
last_name: Pastva
orcid: 0000-0003-1993-0331
- first_name: David
full_name: Šafránek, David
last_name: Šafránek
citation:
ama: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. BNClassifier: Classifying
boolean models by dynamic properties. In: Computational Methods in Systems
Biology. Vol 14971. Springer Nature; 2024:19-26. doi:10.1007/978-3-031-71671-3_2'
apa: 'Beneš, N., Brim, L., Huvar, O., Pastva, S., & Šafránek, D. (2024). BNClassifier:
Classifying boolean models by dynamic properties. In Computational Methods
in Systems Biology (Vol. 14971, pp. 19–26). Springer Nature. https://doi.org/10.1007/978-3-031-71671-3_2'
chicago: 'Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek.
“BNClassifier: Classifying Boolean Models by Dynamic Properties.” In Computational
Methods in Systems Biology, 14971:19–26. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-71671-3_2.'
ieee: 'N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “BNClassifier: Classifying
boolean models by dynamic properties,” in Computational Methods in Systems
Biology, 2024, vol. 14971, pp. 19–26.'
ista: 'Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. 2024. BNClassifier: Classifying
boolean models by dynamic properties. Computational Methods in Systems Biology.
, LNBI, vol. 14971, 19–26.'
mla: 'Beneš, Nikola, et al. “BNClassifier: Classifying Boolean Models by Dynamic
Properties.” Computational Methods in Systems Biology, vol. 14971, Springer
Nature, 2024, pp. 19–26, doi:10.1007/978-3-031-71671-3_2.'
short: N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, in:, Computational Methods
in Systems Biology, Springer Nature, 2024, pp. 19–26.
date_created: 2024-10-06T22:01:12Z
date_published: 2024-09-19T00:00:00Z
date_updated: 2025-09-08T09:54:27Z
day: '19'
department:
- _id: ToHe
doi: 10.1007/978-3-031-71671-3_2
ec_funded: 1
external_id:
isi:
- '001333144400002'
intvolume: ' 14971'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 19-26
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
call_identifier: H2020
grant_number: '101034413'
name: 'IST-BRIDGE: International postdoctoral program'
publication: Computational Methods in Systems Biology
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031716706'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'BNClassifier: Classifying boolean models by dynamic properties'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14971
year: '2024'
...
---
_id: '18206'
abstract:
- lang: eng
text: In the context of in vitro fertilization (IVF), selecting embryos for transfer
is critical in determining pregnancy outcomes, with implantation as the essential
first milestone for a successful pregnancy. This study introduces the Bonna algorithm,
an advanced deep-learning framework engineered to predict embryo implantation
probabilities. The algorithm employs a sophisticated integration of machine-learning
techniques, utilizing MobileNetV2 for pixel and context embedding, a custom Pix2Pix
model for precise segmentation, and a Vision Transformer for additional depth
in embedding. MobileNetV2 was chosen for its robust feature extraction capabilities,
focusing on textures and edges. The custom Pix2Pix model is adapted for precise
segmentation of significant biological features such as the zona pellucida and
blastocyst cavity. The Vision Transformer adds a global perspective, capturing
complex patterns not apparent in local image segments. Tested on a dataset of
images of human blastocysts collected from Ukraine, Israel, and Spain, the Bonna
algorithm was rigorously validated through 10-fold cross-validation to ensure
its robustness and reliability. It demonstrates superior performance with a mean
area under the receiver operating characteristic curve (AUC) of 0.754, significantly
outperforming existing models. The study not only advances predictive accuracy
in embryo selection but also highlights the algorithm’s clinical applicability
due to reliable confidence reporting.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Gilad
full_name: Rave, Gilad
last_name: Rave
- first_name: Daniel E.
full_name: Fordham, Daniel E.
last_name: Fordham
- first_name: Alexander
full_name: Bronstein, Alexander
id: 58f3726e-7cba-11ef-ad8b-e6e8cb3904e6
last_name: Bronstein
orcid: 0000-0001-9699-8730
- first_name: David H.
full_name: Silver, David H.
last_name: Silver
citation:
ama: 'Rave G, Fordham DE, Bronstein AM, Silver DH. Enhancing predictive accuracy
in embryo implantation: The Bonna algorithm and its clinical implications. In:
First International Conference on Artificial Intelligence in Healthcare.
Vol 14976. Springer Nature; 2024:160-171. doi:10.1007/978-3-031-67285-9_12'
apa: 'Rave, G., Fordham, D. E., Bronstein, A. M., & Silver, D. H. (2024). Enhancing
predictive accuracy in embryo implantation: The Bonna algorithm and its clinical
implications. In First International Conference on Artificial Intelligence
in Healthcare (Vol. 14976, pp. 160–171). Swansea, United Kingdom: Springer
Nature. https://doi.org/10.1007/978-3-031-67285-9_12'
chicago: 'Rave, Gilad, Daniel E. Fordham, Alex M. Bronstein, and David H. Silver.
“Enhancing Predictive Accuracy in Embryo Implantation: The Bonna Algorithm and Its
Clinical Implications.” In First International Conference on Artificial Intelligence
in Healthcare, 14976:160–71. Springer Nature, 2024. https://doi.org/10.1007/978-3-031-67285-9_12.'
ieee: 'G. Rave, D. E. Fordham, A. M. Bronstein, and D. H. Silver, “Enhancing predictive
accuracy in embryo implantation: The Bonna algorithm and its clinical implications,”
in First International Conference on Artificial Intelligence in Healthcare,
Swansea, United Kingdom, 2024, vol. 14976, pp. 160–171.'
ista: 'Rave G, Fordham DE, Bronstein AM, Silver DH. 2024. Enhancing predictive accuracy
in embryo implantation: The Bonna algorithm and its clinical implications. First
International Conference on Artificial Intelligence in Healthcare. AIiH: Artificial
Intelligence in Healthcare, LNCS, vol. 14976, 160–171.'
mla: 'Rave, Gilad, et al. “Enhancing Predictive Accuracy in Embryo Implantation:
The Bonna Algorithm and Its Clinical Implications.” First International Conference
on Artificial Intelligence in Healthcare, vol. 14976, Springer Nature, 2024,
pp. 160–71, doi:10.1007/978-3-031-67285-9_12.'
short: G. Rave, D.E. Fordham, A.M. Bronstein, D.H. Silver, in:, First International
Conference on Artificial Intelligence in Healthcare, Springer Nature, 2024, pp.
160–171.
conference:
end_date: 2024-09-06
location: Swansea, United Kingdom
name: 'AIiH: Artificial Intelligence in Healthcare'
start_date: 2024-09-04
date_created: 2024-10-08T12:46:23Z
date_published: 2024-08-15T00:00:00Z
date_updated: 2024-10-09T10:33:39Z
day: '15'
doi: 10.1007/978-3-031-67285-9_12
extern: '1'
intvolume: ' 14976'
language:
- iso: eng
month: '08'
oa_version: None
page: 160-171
publication: First International Conference on Artificial Intelligence in Healthcare
publication_identifier:
eisbn:
- '9783031672859'
eissn:
- 1611-3349
isbn:
- '9783031672842'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Enhancing predictive accuracy in embryo implantation: The Bonna algorithm
and its clinical implications'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14976
year: '2024'
...
---
_id: '12467'
abstract:
- lang: eng
text: Safety and liveness are elementary concepts of computation, and the foundation
of many verification paradigms. The safety-liveness classification of boolean
properties characterizes whether a given property can be falsified by observing
a finite prefix of an infinite computation trace (always for safety, never for
liveness). In quantitative specification and verification, properties assign not
truth values, but quantitative values to infinite traces (e.g., a cost, or the
distance to a boolean property). We introduce quantitative safety and liveness,
and we prove that our definitions induce conservative quantitative generalizations
of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness
decomposition of boolean properties. In particular, we show that every quantitative
property can be written as the pointwise minimum of a quantitative safety property
and a quantitative liveness property. Consequently, like boolean properties, also
quantitative properties can be min-decomposed into safety and liveness parts,
or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover,
quantitative properties can be approximated naturally. We prove that every quantitative
property that has both safe and co-safe approximations can be monitored arbitrarily
precisely by a monitor that uses only a finite number of states.
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
full_name: Mazzocchi, Nicolas Adrien
id: b26baa86-3308-11ec-87b0-8990f34baa85
last_name: Mazzocchi
- first_name: Naci E
full_name: Sarac, Naci E
id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
last_name: Sarac
citation:
ama: 'Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In:
26th International Conference Foundations of Software Science and Computation
Structures. Vol 13992. Springer Nature; 2023:349-370. doi:10.1007/978-3-031-30829-1_17'
apa: 'Henzinger, T. A., Mazzocchi, N. A., & Sarac, N. E. (2023). Quantitative
safety and liveness. In 26th International Conference Foundations of Software
Science and Computation Structures (Vol. 13992, pp. 349–370). Paris, France:
Springer Nature. https://doi.org/10.1007/978-3-031-30829-1_17'
chicago: Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative
Safety and Liveness.” In 26th International Conference Foundations of Software
Science and Computation Structures, 13992:349–70. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30829-1_17.
ieee: T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and
liveness,” in 26th International Conference Foundations of Software Science
and Computation Structures, Paris, France, 2023, vol. 13992, pp. 349–370.
ista: 'Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness.
26th International Conference Foundations of Software Science and Computation
Structures. FOSSACS: Foundations of Software Science and Computation Structures,
LNCS, vol. 13992, 349–370.'
mla: Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” 26th International
Conference Foundations of Software Science and Computation Structures, vol.
13992, Springer Nature, 2023, pp. 349–70, doi:10.1007/978-3-031-30829-1_17.
short: T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference
Foundations of Software Science and Computation Structures, Springer Nature, 2023,
pp. 349–370.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FOSSACS: Foundations of Software Science and Computation Structures'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-01-31T07:23:56Z
date_published: 2023-04-21T00:00:00Z
date_updated: 2025-09-09T12:21:08Z
day: '21'
ddc:
- '000'
department:
- _id: GradSch
- _id: ToHe
doi: 10.1007/978-3-031-30829-1_17
ec_funded: 1
external_id:
arxiv:
- '2301.11175'
isi:
- '001288609300017'
file:
- access_level: open_access
checksum: 981025aed580b6b27c426cb8856cf63e
content_type: application/pdf
creator: esarac
date_created: 2023-01-31T07:22:21Z
date_updated: 2023-01-31T07:22:21Z
file_id: '12468'
file_name: qsl.pdf
file_size: 449027
relation: main_file
success: 1
- access_level: open_access
checksum: f16e2af1e0eb243158ab0f0fe74e7d5a
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T10:28:09Z
date_updated: 2023-06-19T10:28:09Z
file_id: '13153'
file_name: 2023_LNCS_HenzingerT.pdf
file_size: 1048171
relation: main_file
success: 1
file_date_updated: 2023-06-19T10:28:09Z
has_accepted_license: '1'
intvolume: ' 13992'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 349-370
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 26th International Conference Foundations of Software Science and Computation
Structures
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308284'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative safety and liveness
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13992
year: '2023'
...
---
_id: '12854'
abstract:
- lang: eng
text: "The main idea behind BUBAAK is to run multiple program analyses in parallel
and use runtime monitoring and enforcement to observe and control their progress
in real time. The analyses send information about (un)explored states of the program
and discovered invariants to a monitor. The monitor processes the received data
and can force an analysis to stop the search of certain program parts (which have
already been analyzed by other analyses), or to make it utilize a program invariant
found by another analysis.\r\nAt SV-COMP 2023, the implementation of data exchange
between the monitor and the analyses was not yet completed, which is why BUBAAK
only ran several analyses in parallel, without any coordination. Still, BUBAAK
won the meta-category FalsificationOverall and placed very well in several other
(sub)-categories of the competition."
acknowledgement: This work was supported by the ERC-2020-AdG 10102009 grant.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers.
In: Tools and Algorithms for the Construction and Analysis of Systems.
Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32'
apa: 'Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of
program verifiers. In Tools and Algorithms for the Construction and Analysis
of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32'
chicago: 'Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of
Program Verifiers.” In Tools and Algorithms for the Construction and Analysis
of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.'
ieee: 'M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,”
in Tools and Algorithms for the Construction and Analysis of Systems, Paris,
France, 2023, vol. 13994, pp. 535–540.'
ista: 'Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers.
Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994,
535–540.'
mla: 'Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program
Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32.'
short: M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2023, pp. 535–540.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-04-20T08:22:53Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2025-09-09T12:24:56Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_32
ec_funded: 1
external_id:
isi:
- '001288698100041'
file:
- access_level: open_access
checksum: 120d2c2a38384058ad0630fdf8288312
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T06:58:36Z
date_updated: 2023-04-25T06:58:36Z
file_id: '12864'
file_name: 2023_LNCS_Chalupa.pdf
file_size: 16096413
relation: main_file
success: 1
file_date_updated: 2023-04-25T06:58:36Z
has_accepted_license: '1'
intvolume: ' 13994'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 535-540
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783031308208'
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Bubaak: Runtime monitoring of program verifiers'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13994
year: '2023'
...
---
_id: '12856'
abstract:
- lang: eng
text: "As the complexity and criticality of software increase every year, so does
the importance of run-time monitoring. Third-party monitoring, with limited knowledge
of the monitored software, and best-effort monitoring, which keeps pace with the
monitored software, are especially valuable, yet underexplored areas of run-time
monitoring. Most existing monitoring frameworks do not support their combination
because they either require access to the monitored code for instrumentation purposes
or the processing of all observed events, or both.\r\n\r\nWe present a middleware
framework, VAMOS, for the run-time monitoring of software which is explicitly
designed to support third-party and best-effort scenarios. The design goals of
VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the
ability to monitor black-box code through a variety of different event channels,
and the connectability to monitors written in different specification languages),
and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker
and event recognition systems with aspects of stream processing systems.\r\nWe
implemented a prototype toolchain for VAMOS and conducted experiments including
a case study of monitoring for data races. The results indicate that VAMOS enables
writing useful yet efficient monitors, is compatible with a variety of event sources
and monitor specifications, and simplifies key aspects of setting up a monitoring
system from scratch."
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093. The
authors would like to thank the anonymous FASE reviewers for their valuable feedback
and suggestions.
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: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Stefanie
full_name: Muroya Lei, Stefanie
id: a376de31-8972-11ed-ae7b-d0251c13c8ff
last_name: Muroya Lei
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
citation:
ama: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort
third-party monitoring. In: Fundamental Approaches to Software Engineering.
Vol 13991. Springer Nature; 2023:260-281. doi:10.1007/978-3-031-30826-0_15'
apa: 'Chalupa, M., Mühlböck, F., Muroya Lei, S., & Henzinger, T. A. (2023).
Vamos: Middleware for best-effort third-party monitoring. In Fundamental Approaches
to Software Engineering (Vol. 13991, pp. 260–281). Paris, France: Springer
Nature. https://doi.org/10.1007/978-3-031-30826-0_15'
chicago: 'Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger.
“Vamos: Middleware for Best-Effort Third-Party Monitoring.” In Fundamental
Approaches to Software Engineering, 13991:260–81. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30826-0_15.'
ieee: 'M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware
for best-effort third-party monitoring,” in Fundamental Approaches to Software
Engineering, Paris, France, 2023, vol. 13991, pp. 260–281.'
ista: 'Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware
for best-effort third-party monitoring. Fundamental Approaches to Software Engineering.
FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.'
mla: 'Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.”
Fundamental Approaches to Software Engineering, vol. 13991, Springer Nature,
2023, pp. 260–81, doi:10.1007/978-3-031-30826-0_15.'
short: M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental
Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281.
conference:
end_date: 2023-04-27
location: Paris, France
name: 'FASE: Fundamental Approaches to Software Engineering'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-04-20T08:29:42Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2025-09-09T12:25:29Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30826-0_15
ec_funded: 1
external_id:
isi:
- '001284136600015'
file:
- access_level: open_access
checksum: 17a7c8e08be609cf2408d37ea55e322c
content_type: application/pdf
creator: dernst
date_created: 2023-04-25T07:16:36Z
date_updated: 2023-04-25T07:16:36Z
file_id: '12865'
file_name: 2023_LNCS_ChalupaM.pdf
file_size: 580828
relation: main_file
success: 1
file_date_updated: 2023-04-25T07:16:36Z
has_accepted_license: '1'
intvolume: ' 13991'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 260-281
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: Fundamental Approaches to Software Engineering
publication_identifier:
eisbn:
- '9783031308260'
eissn:
- 1611-3349
isbn:
- '9783031308253'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '18169'
relation: later_version
status: public
- id: '12407'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: 'Vamos: Middleware for best-effort third-party monitoring'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13991
year: '2023'
...
---
_id: '13139'
abstract:
- lang: eng
text: A classical problem for Markov chains is determining their stationary (or
steady-state) distribution. This problem has an equally classical solution based
on eigenvectors and linear equation systems. However, this approach does not scale
to large instances, and iterative solutions are desirable. It turns out that a
naive approach, as used by current model checkers, may yield completely wrong
results. We present a new approach, which utilizes recent advances in partial
exploration and mean payoff computation to obtain a correct, converging approximation.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
citation:
ama: 'Meggendorfer T. Correct approximation of stationary distributions. In: TACAS
2023: Tools and Algorithms for the Construction and Analysis of Systems. Vol
13993. Springer Nature; 2023:489-507. doi:10.1007/978-3-031-30823-9_25'
apa: 'Meggendorfer, T. (2023). Correct approximation of stationary distributions.
In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems
(Vol. 13993, pp. 489–507). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30823-9_25'
chicago: 'Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.”
In TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
13993:489–507. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30823-9_25.'
ieee: 'T. Meggendorfer, “Correct approximation of stationary distributions,” in
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
Paris, France, 2023, vol. 13993, pp. 489–507.'
ista: 'Meggendorfer T. 2023. Correct approximation of stationary distributions.
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
vol. 13993, 489–507.'
mla: 'Meggendorfer, Tobias. “Correct Approximation of Stationary Distributions.”
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13993, Springer Nature, 2023, pp. 489–507, doi:10.1007/978-3-031-30823-9_25.'
short: 'T. Meggendorfer, in:, TACAS 2023: Tools and Algorithms for the Construction
and Analysis of Systems, Springer Nature, 2023, pp. 489–507.'
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
corr_author: '1'
date_created: 2023-06-18T22:00:46Z
date_published: 2023-04-22T00:00:00Z
date_updated: 2025-09-09T12:28:12Z
day: '22'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-30823-9_25
external_id:
arxiv:
- '2301.08137'
isi:
- '001288688000025'
file:
- access_level: open_access
checksum: 59f707a3949c03793251b0d04c62542a
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T07:18:40Z
date_updated: 2023-06-19T07:18:40Z
file_id: '13148'
file_name: 2023_LNCS_Meggendorfer.pdf
file_size: 521951
relation: main_file
success: 1
file_date_updated: 2023-06-19T07:18:40Z
has_accepted_license: '1'
intvolume: ' 13993'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 489-507
publication: 'TACAS 2023: Tools and Algorithms for the Construction and Analysis of
Systems'
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308222'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14990'
relation: research_data
status: public
scopus_import: '1'
status: public
title: Correct approximation of stationary distributions
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13993
year: '2023'
...
---
_id: '13141'
abstract:
- lang: eng
text: "We automatically compute a new class of environment assumptions in two-player
turn-based finite graph games which characterize an “adequate cooperation” needed
from the environment to allow the system player to win. Given an ω-regular winning
condition Φ for the system player, we compute an ω-regular assumption Ψ for the
environment player, such that (i) every environment strategy compliant with Ψ
allows the system to fulfill Φ (sufficiency), (ii) Ψ\r\n can be fulfilled by the
environment for every strategy of the system (implementability), and (iii) Ψ does
not prevent any cooperative strategy choice (permissiveness).\r\nFor parity games,
which are canonical representations of ω-regular games, we present a polynomial-time
algorithm for the symbolic computation of adequately permissive assumptions and
show that our algorithm runs faster and produces better assumptions than existing
approaches—both theoretically and empirically. To the best of our knowledge, for
ω\r\n-regular games, we provide the first algorithm to compute sufficient and
implementable environment assumptions that are also permissive."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ashwani
full_name: Anand, Ashwani
last_name: Anand
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Satya Prakash
full_name: Nayak, Satya Prakash
last_name: Nayak
- first_name: Anne Kathrin
full_name: Schmuck, Anne Kathrin
last_name: Schmuck
citation:
ama: 'Anand A, Mallik K, Nayak SP, Schmuck AK. Computing adequately permissive assumptions
for synthesis. In: TACAS 2023: Tools and Algorithms for the Construction and
Analysis of Systems. Vol 13994. Springer Nature; 2023:211-228. doi:10.1007/978-3-031-30820-8_15'
apa: 'Anand, A., Mallik, K., Nayak, S. P., & Schmuck, A. K. (2023). Computing
adequately permissive assumptions for synthesis. In TACAS 2023: Tools and Algorithms
for the Construction and Analysis of Systems (Vol. 13994, pp. 211–228). Paris,
France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_15'
chicago: 'Anand, Ashwani, Kaushik Mallik, Satya Prakash Nayak, and Anne Kathrin
Schmuck. “Computing Adequately Permissive Assumptions for Synthesis.” In TACAS
2023: Tools and Algorithms for the Construction and Analysis of Systems, 13994:211–28.
Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_15.'
ieee: 'A. Anand, K. Mallik, S. P. Nayak, and A. K. Schmuck, “Computing adequately
permissive assumptions for synthesis,” in TACAS 2023: Tools and Algorithms
for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994,
pp. 211–228.'
ista: 'Anand A, Mallik K, Nayak SP, Schmuck AK. 2023. Computing adequately permissive
assumptions for synthesis. TACAS 2023: Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of Systems, LNCS, vol. 13994, 211–228.'
mla: 'Anand, Ashwani, et al. “Computing Adequately Permissive Assumptions for Synthesis.”
TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems,
vol. 13994, Springer Nature, 2023, pp. 211–28, doi:10.1007/978-3-031-30820-8_15.'
short: 'A. Anand, K. Mallik, S.P. Nayak, A.K. Schmuck, in:, TACAS 2023: Tools and
Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023,
pp. 211–228.'
conference:
end_date: 2023-04-27
location: Paris, France
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2023-04-22
date_created: 2023-06-18T22:00:47Z
date_published: 2023-04-20T00:00:00Z
date_updated: 2025-09-09T12:30:00Z
day: '20'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-30820-8_15
external_id:
isi:
- '001288698100015'
file:
- access_level: open_access
checksum: 60dcafc1b4f6f070be43bad3fe877974
content_type: application/pdf
creator: dernst
date_created: 2023-06-19T08:43:21Z
date_updated: 2023-06-19T08:43:21Z
file_id: '13151'
file_name: 2023_LNCS_Anand.pdf
file_size: 521425
relation: main_file
success: 1
file_date_updated: 2023-06-19T08:43:21Z
has_accepted_license: '1'
intvolume: ' 13994'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 211-228
publication: 'TACAS 2023: Tools and Algorithms for the Construction and Analysis of
Systems'
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783031308192'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing adequately permissive assumptions for synthesis
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13994
year: '2023'
...