[{"doi":"10.1007/978-3-031-90653-4_7","oa":1,"acknowledgement":"This project has received funding from the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12, a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, the DFG RTG 378803395 (ConVeY), the EU’s Horizon 2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement Nos. 101034413 (IST-BRIDGE) and 101008233 (MISSION), and the DFG RTG 2236 (UnRAVeL). Experiments were performed with computing resources granted by RWTH Aachen University under project rwth1632.","volume":15697,"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Tim","last_name":"Quatmann","full_name":"Quatmann, Tim"},{"last_name":"Schäffeler","full_name":"Schäffeler, Maximilian","first_name":"Maximilian"},{"last_name":"Weininger","full_name":"Weininger, Maximilian","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881"},{"last_name":"Winkler","full_name":"Winkler, Tobias","first_name":"Tobias"},{"first_name":"Daniel","id":"d8ebc24a-3f98-11f0-9044-8296d4f39ab3","last_name":"Zilken","full_name":"Zilken, Daniel"}],"department":[{"_id":"KrCh"}],"month":"05","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","grant_number":"101034413"}],"article_processing_charge":"No","tmp":{"short":"CC BY (4.0)","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)"},"corr_author":"1","publisher":"Springer Nature","related_material":{"record":[{"status":"public","id":"19771","relation":"research_data"}]},"conference":{"location":"Hamilton, ON, Canada","end_date":"2025-05-08","start_date":"2025-05-03","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"publication_status":"published","file":[{"date_updated":"2025-06-02T10:49:52Z","relation":"main_file","creator":"dernst","file_id":"19772","checksum":"64b7f46ef05649b87b827248045c7645","file_name":"2025_TACAS_ChatterjeeKrish.pdf","content_type":"application/pdf","success":1,"file_size":732136,"date_created":"2025-06-02T10:49:52Z","access_level":"open_access"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031906527"]},"arxiv":1,"date_created":"2025-05-25T22:17:09Z","alternative_title":["LNCS"],"title":"Fixed point certificates for reachability and expected rewards in MDPs","OA_type":"hybrid","oa_version":"Published Version","file_date_updated":"2025-06-02T10:49:52Z","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","date_updated":"2025-06-02T10:55:34Z","status":"public","page":"130-151","ec_funded":1,"scopus_import":"1","external_id":{"arxiv":["2501.11467"]},"abstract":[{"text":"The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates—lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.","lang":"eng"}],"_id":"19743","language":[{"iso":"eng"}],"quality_controlled":"1","type":"conference","citation":{"ista":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. 2025. Fixed point certificates for reachability and expected rewards in MDPs. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 130–151.","ama":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. Fixed point certificates for reachability and expected rewards in MDPs. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:130-151. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>","chicago":"Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:130–51. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>.","ieee":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D. Zilken, “Fixed point certificates for reachability and expected rewards in MDPs,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 130–151.","short":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 130–151.","mla":"Chatterjee, Krishnendu, et al. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 130–51, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>.","apa":"Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T., &#38; Zilken, D. (2025). Fixed point certificates for reachability and expected rewards in MDPs. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 130–151). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>"},"day":"01","has_accepted_license":"1","intvolume":"     15697","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","OA_place":"publisher","date_published":"2025-05-01T00:00:00Z"},{"publication_identifier":{"isbn":["9783031906527"],"eissn":["1611-3349"],"issn":["0302-9743"]},"arxiv":1,"oa_version":"Published Version","OA_type":"hybrid","alternative_title":["LNCS"],"date_created":"2025-05-25T22:17:10Z","title":"Refuting equivalence in probabilistic programs with conditioning","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2025-05-03","end_date":"2025-05-08","location":"Hamilton, ON, Canada"},"publication_status":"published","file":[{"date_created":"2025-06-02T11:13:49Z","file_size":532181,"content_type":"application/pdf","success":1,"access_level":"open_access","relation":"main_file","file_id":"19773","date_updated":"2025-06-02T11:13:49Z","creator":"dernst","file_name":"2025_TACAS_Chatterjee_Goharshadi.pdf","checksum":"7dcd85e7e753bfa994c10b3cf9ebc185"}],"publisher":"Springer Nature","tmp":{"short":"CC BY (4.0)","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)"},"corr_author":"1","article_processing_charge":"No","acknowledgement":"This work was partially supported by ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12. Petr Novotný is supported by the Czech Science Foundation grant no. GA23-06963S.","doi":"10.1007/978-3-031-90653-4_14","oa":1,"project":[{"grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"month":"05","department":[{"_id":"KrCh"}],"volume":15697,"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","full_name":"Kafshdar Goharshadi, Ehsan","last_name":"Kafshdar Goharshadi"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotný","full_name":"Novotný, Petr"},{"first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","last_name":"Zikelic","full_name":"Zikelic, Dorde"}],"year":"2025","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"     15697","date_published":"2025-05-01T00:00:00Z","OA_place":"publisher","type":"conference","quality_controlled":"1","language":[{"iso":"eng"}],"_id":"19744","abstract":[{"text":"We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature.","lang":"eng"}],"external_id":{"arxiv":["2501.06579"]},"has_accepted_license":"1","day":"01","citation":{"apa":"Chatterjee, K., Goharshady, E., Novotný, P., &#38; Zikelic, D. (2025). Refuting equivalence in probabilistic programs with conditioning. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 279–300). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">https://doi.org/10.1007/978-3-031-90653-4_14</a>","mla":"Chatterjee, Krishnendu, et al. “Refuting Equivalence in Probabilistic Programs with Conditioning.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 279–300, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">10.1007/978-3-031-90653-4_14</a>.","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Refuting equivalence in probabilistic programs with conditioning,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 279–300.","short":"K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 279–300.","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic. “Refuting Equivalence in Probabilistic Programs with Conditioning.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:279–300. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">https://doi.org/10.1007/978-3-031-90653-4_14</a>.","ama":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. Refuting equivalence in probabilistic programs with conditioning. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:279-300. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">10.1007/978-3-031-90653-4_14</a>","ista":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2025. Refuting equivalence in probabilistic programs with conditioning. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 279–300."},"page":"279-300","status":"public","scopus_import":"1","ec_funded":1,"file_date_updated":"2025-06-02T11:13:49Z","date_updated":"2025-06-02T11:16:13Z","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"publisher":"Springer Nature","article_processing_charge":"No","corr_author":"1","oa":1,"doi":"10.1007/978-3-032-12290-2_6","acknowledgement":"Jesko Dujmovic: Funded by the European Union (ERC, LACONIC, 101041207). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.\r\nChristoph U. Günther and Krzysztof Pietrzak: This research was funded in whole or in part by the Austrian Science Fund (FWF) 10.55776/F85. For open access purposes, the author has applied a CC BY public copyright license to any author-accepted manuscript version arising from this submission.","department":[{"_id":"KrPi"}],"month":"12","project":[{"grant_number":"F8509","_id":"34a34d57-11ca-11ed-8bc3-a2688a8724e1","name":"Security and Privacy by Design for Complex Systems"}],"author":[{"first_name":"Jesko","last_name":"Dujmovic","full_name":"Dujmovic, Jesko"},{"last_name":"Günther","full_name":"Günther, Christoph Ullrich","first_name":"Christoph Ullrich","id":"ec98511c-eb8e-11eb-b029-edd25d7271a1"},{"last_name":"Pietrzak","full_name":"Pietrzak, Krzysztof Z","orcid":"0000-0002-9139-1654","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","first_name":"Krzysztof Z"}],"volume":16271,"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783032122896"]},"OA_type":"green","oa_version":"Preprint","alternative_title":["LNCS"],"title":"Space-deniable proofs","date_created":"2025-12-21T23:01:33Z","conference":{"name":"TCC: Theory of Cryptography","start_date":"2025-12-01","end_date":"2025-12-05","location":"Aarhus, Denmark"},"publication_status":"published","page":"171-202","status":"public","scopus_import":"1","date_updated":"2025-12-29T11:44:16Z","publication":"23rd International Conference on Theory of Cryptography","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","intvolume":"     16271","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2025/1723"}],"OA_place":"repository","date_published":"2025-12-05T00:00:00Z","quality_controlled":"1","type":"conference","_id":"20844","abstract":[{"lang":"eng","text":"We introduce and construct a new proof system called Non-interactive Arguments of Knowledge or Space (NArKoS), where a space-bounded prover can convince a verifier they know a secret, while having access to sufficient space allows one to forge indistinguishable proofs without the secret.\r\nAn application of NArKoS are space-deniable proofs, which are proofs of knowledge (say for authentication in access control) that are sound when executed by a lightweight device like a smart-card or an RFID chip that cannot have much storage, but are deniable (in the strong sense of online deniability) as the verifier, like a card reader, can efficiently forge such proofs.\r\nWe construct NArKoS in the random oracle model using an OR-proof combining a sigma protocol (for the proof of knowledge of the secret) with a new proof system called simulatable Proof of Transient Space (simPoTS). We give two different constructions of simPoTS, one based on labelling graphs with high pebbling complexity, a technique used in the construction of memory-hard functions and proofs of space, and a more practical construction based on the verifiable space-hard functions from TCC’24 where a prover must compute a root of a sparse polynomial. In both cases, the main challenge is making the proofs efficiently simulatable."}],"language":[{"iso":"eng"}],"day":"05","citation":{"chicago":"Dujmovic, Jesko, Christoph Ullrich Günther, and Krzysztof Z Pietrzak. “Space-Deniable Proofs.” In <i>23rd International Conference on Theory of Cryptography</i>, 16271:171–202. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-12290-2_6\">https://doi.org/10.1007/978-3-032-12290-2_6</a>.","ama":"Dujmovic J, Günther CU, Pietrzak KZ. Space-deniable proofs. In: <i>23rd International Conference on Theory of Cryptography</i>. Vol 16271. Springer Nature; 2025:171-202. doi:<a href=\"https://doi.org/10.1007/978-3-032-12290-2_6\">10.1007/978-3-032-12290-2_6</a>","ista":"Dujmovic J, Günther CU, Pietrzak KZ. 2025. Space-deniable proofs. 23rd International Conference on Theory of Cryptography. TCC: Theory of Cryptography, LNCS, vol. 16271, 171–202.","apa":"Dujmovic, J., Günther, C. U., &#38; Pietrzak, K. Z. (2025). Space-deniable proofs. In <i>23rd International Conference on Theory of Cryptography</i> (Vol. 16271, pp. 171–202). Aarhus, Denmark: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-12290-2_6\">https://doi.org/10.1007/978-3-032-12290-2_6</a>","mla":"Dujmovic, Jesko, et al. “Space-Deniable Proofs.” <i>23rd International Conference on Theory of Cryptography</i>, vol. 16271, Springer Nature, 2025, pp. 171–202, doi:<a href=\"https://doi.org/10.1007/978-3-032-12290-2_6\">10.1007/978-3-032-12290-2_6</a>.","ieee":"J. Dujmovic, C. U. Günther, and K. Z. Pietrzak, “Space-deniable proofs,” in <i>23rd International Conference on Theory of Cryptography</i>, Aarhus, Denmark, 2025, vol. 16271, pp. 171–202.","short":"J. Dujmovic, C.U. Günther, K.Z. Pietrzak, in:, 23rd International Conference on Theory of Cryptography, Springer Nature, 2025, pp. 171–202."}},{"conference":{"start_date":"2025-12-01","name":"TCC: Theory of Cryptography","location":"Aarhus, Denmark","end_date":"2025-12-05"},"publication_status":"published","title":"Zeroizing attacks against evasive and circular evasive LWE","date_created":"2025-12-21T23:01:33Z","alternative_title":["LNCS"],"oa_version":"Preprint","OA_type":"green","publication_identifier":{"isbn":["9783032122926"],"eissn":["1611-3349"],"issn":["0302-9743"]},"author":[{"first_name":"Shweta","last_name":"Agrawal","full_name":"Agrawal, Shweta"},{"first_name":"Anuja","full_name":"Modi, Anuja","last_name":"Modi"},{"full_name":"Yadav, Anshu","last_name":"Yadav","id":"dc8f1524-403e-11ee-bf07-9649ad996e21","first_name":"Anshu"},{"full_name":"Yamada, Shota","last_name":"Yamada","first_name":"Shota"}],"volume":16269,"month":"12","department":[{"_id":"KrPi"}],"acknowledgement":"We thank Rachel Lin for expressing concern about the applicability of “HJL-style” attacks [15] on the construction in [2] during a talk by the first author about [2]. This was the starting point of the investigation that led us to develop the attack in [5, Sec 4.1]. The first author also thanks Hoeteck Wee for sharing his rationale for introducing evasive LWE.\r\nThe first author is supported by the CyStar center of excellence, the VHAR faculty chair, and the C3iHub fellowship. The third author thanks Cystar, IIT Madras, for supporting a visit to IIT Madras during which the collaboration was initiated. The 4th author is partly supported by JST CREST Grant Number JPMJCR22M1.","oa":1,"doi":"10.1007/978-3-032-12293-3_9","article_processing_charge":"No","publisher":"Springer Nature","day":"05","citation":{"chicago":"Agrawal, Shweta, Anuja Modi, Anshu Yadav, and Shota Yamada. “Zeroizing Attacks against Evasive and Circular Evasive LWE.” In <i>23rd International Conference on Theory of Cryptography</i>, 16269:259–90. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-12293-3_9\">https://doi.org/10.1007/978-3-032-12293-3_9</a>.","ista":"Agrawal S, Modi A, Yadav A, Yamada S. 2025. Zeroizing attacks against evasive and circular evasive LWE. 23rd International Conference on Theory of Cryptography. TCC: Theory of Cryptography, LNCS, vol. 16269, 259–290.","ama":"Agrawal S, Modi A, Yadav A, Yamada S. Zeroizing attacks against evasive and circular evasive LWE. In: <i>23rd International Conference on Theory of Cryptography</i>. Vol 16269. Springer Nature; 2025:259-290. doi:<a href=\"https://doi.org/10.1007/978-3-032-12293-3_9\">10.1007/978-3-032-12293-3_9</a>","apa":"Agrawal, S., Modi, A., Yadav, A., &#38; Yamada, S. (2025). Zeroizing attacks against evasive and circular evasive LWE. In <i>23rd International Conference on Theory of Cryptography</i> (Vol. 16269, pp. 259–290). Aarhus, Denmark: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-12293-3_9\">https://doi.org/10.1007/978-3-032-12293-3_9</a>","ieee":"S. Agrawal, A. Modi, A. Yadav, and S. Yamada, “Zeroizing attacks against evasive and circular evasive LWE,” in <i>23rd International Conference on Theory of Cryptography</i>, Aarhus, Denmark, 2025, vol. 16269, pp. 259–290.","short":"S. Agrawal, A. Modi, A. Yadav, S. Yamada, in:, 23rd International Conference on Theory of Cryptography, Springer Nature, 2025, pp. 259–290.","mla":"Agrawal, Shweta, et al. “Zeroizing Attacks against Evasive and Circular Evasive LWE.” <i>23rd International Conference on Theory of Cryptography</i>, vol. 16269, Springer Nature, 2025, pp. 259–90, doi:<a href=\"https://doi.org/10.1007/978-3-032-12293-3_9\">10.1007/978-3-032-12293-3_9</a>."},"_id":"20845","abstract":[{"text":"We develop new attacks against the Evasive LWE family of assumptions, in both the public and private-coin regime. To the best of our knowledge, ours are the first attacks against Evasive LWE in the public-coin regime, for any instantiation from the family. Our attacks are summarized below.\r\n\r\nPublic-Coin Attacks.\r\n1.The recent work by Hseih, Lin and Luo [17] constructed the first Attribute Based Encryption (ABE) for unbounded depth circuits by relying on the “circular” evasive LWE assumption. This assumption has been popularly considered as a safe, public-coin instance of Evasive LWE in contrast to its “private-coin” cousins (for instance, see [10, 11]).\r\nWe provide the first attack against this assumption, challenging the widely held belief that this is a public-coin assumption.\r\n2. We demonstrate a counter-example against vanilla public-coin evasive LWE by Wee [26] in an unnatural parameter regime. Our attack crucially relies on the error in the pre-condition being larger than the error in the post-condition, necessitating a refinement of the assumption.\r\n\r\nPrivate-Coin Attacks.\r\n1. The recent work by Agrawal, Kumari and Yamada [2] constructed the first functional encryption scheme for pseudorandom functionalities (PRFE) and extended this to obfuscation for pseudorandom functionalities (PRIO) [4] by relying on private-coin evasive LWE. We provide a new attack against the assumption stated in the first posting of their work (subsequently refined to avoid these attacks).\r\n2. The recent work by Branco et al. [8] (concurrently to [4]) provides a construction of obfuscation for pseudorandom functionalities by relying on private-coin evasive LWE. We provide a new attack against their stated assumption.\r\n3. Branco et al. [8] showed that there exist contrived, “self-referential” classes of pseudorandom functionalities for which pseudorandom obfuscation cannot exist. We extend their techniques to develop an analogous result for pseudorandom functional encryption.\r\n\r\nWhile Evasive LWE was developed to specifically avoid “zeroizing attacks”, our work shows that in certain settings, such attacks can still apply.","lang":"eng"}],"language":[{"iso":"eng"}],"type":"conference","quality_controlled":"1","date_published":"2025-12-05T00:00:00Z","OA_place":"repository","main_file_link":[{"url":"https://eprint.iacr.org/2025/375","open_access":"1"}],"intvolume":"     16269","year":"2025","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"23rd International Conference on Theory of Cryptography","date_updated":"2025-12-29T11:51:13Z","scopus_import":"1","status":"public","page":"259-290"},{"day":"05","citation":{"chicago":"Brandt, Nicholas, Miguel Cueto Noval, Christoph Ullrich Günther, Akin Ünal, and Stella Wohnig. “Constrained Verifiable Random Functions without Obfuscation and Friends.” In <i>23rd International Conference on Theory of Cryptography</i>, 16271:478–511. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-12290-2_16\">https://doi.org/10.1007/978-3-032-12290-2_16</a>.","ista":"Brandt N, Cueto Noval M, Günther CU, Ünal A, Wohnig S. 2025. Constrained verifiable random functions without obfuscation and friends. 23rd International Conference on Theory of Cryptography. TCC: Theory of Cryptography, LNCS, vol. 16271, 478–511.","ama":"Brandt N, Cueto Noval M, Günther CU, Ünal A, Wohnig S. Constrained verifiable random functions without obfuscation and friends. In: <i>23rd International Conference on Theory of Cryptography</i>. Vol 16271. Springer Nature; 2025:478-511. doi:<a href=\"https://doi.org/10.1007/978-3-032-12290-2_16\">10.1007/978-3-032-12290-2_16</a>","apa":"Brandt, N., Cueto Noval, M., Günther, C. U., Ünal, A., &#38; Wohnig, S. (2025). Constrained verifiable random functions without obfuscation and friends. In <i>23rd International Conference on Theory of Cryptography</i> (Vol. 16271, pp. 478–511). Aarhus, Denmark: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-12290-2_16\">https://doi.org/10.1007/978-3-032-12290-2_16</a>","ieee":"N. Brandt, M. Cueto Noval, C. U. Günther, A. Ünal, and S. Wohnig, “Constrained verifiable random functions without obfuscation and friends,” in <i>23rd International Conference on Theory of Cryptography</i>, Aarhus, Denmark, 2025, vol. 16271, pp. 478–511.","short":"N. Brandt, M. Cueto Noval, C.U. Günther, A. Ünal, S. Wohnig, in:, 23rd International Conference on Theory of Cryptography, Springer Nature, 2025, pp. 478–511.","mla":"Brandt, Nicholas, et al. “Constrained Verifiable Random Functions without Obfuscation and Friends.” <i>23rd International Conference on Theory of Cryptography</i>, vol. 16271, Springer Nature, 2025, pp. 478–511, doi:<a href=\"https://doi.org/10.1007/978-3-032-12290-2_16\">10.1007/978-3-032-12290-2_16</a>."},"type":"conference","quality_controlled":"1","abstract":[{"text":"CVRFs are PRFs that unify the properties of verifiable and constrained PRFs. Since they were introduced concurrently by Fuchsbauer and Chandran-Raghuraman-Vinayagamurthy in 2014, it has been an open problem to construct CVRFs without using heavy machinery such as multilinear maps, obfuscation or functional encryption.\r\nWe solve this problem by constructing a prefix-constrained verifiable PRF that does not rely on the aforementioned assumptions. Essentially, our construction is a verifiable version of the Goldreich-Goldwasser-Micali PRF. To achieve verifiability we leverage degree-2 algebraic PRGs and bilinear groups. In short, proofs consist of intermediate values of the Goldreich-Goldwasser-Micali PRF raised to the exponents of group elements. These outputs can be verified using pairings since the underlying PRG is of degree 2.\r\nWe prove the selective security of our construction under the Decisional Square Diffie-Hellman (DSDH) assumption and a new assumption, which we dub recursive Decisional Diffie-Hellman (recursive DDH).\r\nWe prove the soundness of recursive DDH in the generic group model assuming the hardness of the Multivariate Quadratic (MQ) problem and a new variant thereof, which we call MQ+.\r\nLast, in terms of applications, we observe that our CVRF is also an exponent (C)VRF in the plain model. Exponent VRFs were recently introduced by Boneh et al. (Eurocrypt’25) with various applications to threshold cryptography in mind. In addition to that, we give further applications for prefix-CVRFs in the blockchain setting, namely, stake-pooling and compressible randomness beacons.","lang":"eng"}],"_id":"20846","language":[{"iso":"eng"}],"main_file_link":[{"url":"https://eprint.iacr.org/2025/1045","open_access":"1"}],"date_published":"2025-12-05T00:00:00Z","OA_place":"repository","year":"2025","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"     16271","date_updated":"2025-12-29T11:11:29Z","publication":"23rd International Conference on Theory of Cryptography","scopus_import":"1","page":"478-511","status":"public","publication_status":"published","conference":{"name":"TCC: Theory of Cryptography","start_date":"2025-12-01","end_date":"2025-12-05","location":"Aarhus, Denmark"},"oa_version":"Preprint","OA_type":"green","date_created":"2025-12-21T23:01:34Z","title":"Constrained verifiable random functions without obfuscation and friends","alternative_title":["LNCS"],"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783032122896"]},"project":[{"name":"Security and Privacy by Design for Complex Systems","grant_number":"F8509","_id":"34a34d57-11ca-11ed-8bc3-a2688a8724e1"}],"department":[{"_id":"KrPi"}],"month":"12","volume":16271,"author":[{"full_name":"Brandt, Nicholas","last_name":"Brandt","first_name":"Nicholas"},{"first_name":"Miguel","id":"ffc563a3-f6e0-11ea-865d-e3cce03d17cc","orcid":"0000-0002-2505-4246","last_name":"Cueto Noval","full_name":"Cueto Noval, Miguel"},{"id":"ec98511c-eb8e-11eb-b029-edd25d7271a1","first_name":"Christoph Ullrich","full_name":"Günther, Christoph Ullrich","last_name":"Günther"},{"last_name":"Ünal","full_name":"Ünal, Akin","id":"f6b56fb6-dc63-11ee-9dbf-f6780863a85a","first_name":"Akin","orcid":"0000-0002-8929-0221"},{"full_name":"Wohnig, Stella","last_name":"Wohnig","first_name":"Stella"}],"acknowledgement":"We thank Jonas Steinbach and Gertjan De Mulder for helpful discussions on BIP 32, Dennis Hofheinz and Julia Kastner for helpful discussions on early prototypes of our CVRF, and Klaus Kraßnitzer for running pairing benchmarks on his MacBook Pro.\r\nChristoph U. Günther: This research was funded in whole or in part by the Austrian Science Fund (FWF) 10.55776/F85. For open access purposes, the author has applied a CC BY public copyright license to any author-accepted manuscript version arising from this submission.","oa":1,"doi":"10.1007/978-3-032-12290-2_16","publisher":"Springer Nature","corr_author":"1","article_processing_charge":"No"},{"oa":1,"doi":"10.1007/978-3-032-05435-7_1","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","month":"09","department":[{"_id":"ToHe"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"author":[{"orcid":"0000-0002-0783-904X","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","first_name":"Filip","full_name":"Cano Cordoba, Filip","last_name":"Cano Cordoba"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"orcid":"0000-0001-8974-2542","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","first_name":"Konstantin","last_name":"Kueffner","full_name":"Kueffner, Konstantin"}],"volume":16087,"publisher":"Springer Nature","article_processing_charge":"No","corr_author":"1","publication_status":"published","conference":{"end_date":"2025-09-19","location":"Graz, Austria","name":"RV: Runtime Verification","start_date":"2025-09-15"},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783032054357"]},"arxiv":1,"OA_type":"green","oa_version":"Preprint","alternative_title":["LNCS"],"date_created":"2026-01-29T16:01:41Z","title":"Algorithmic fairness: A runtime perspective","publication":"25th International Conference on Runtime Verification","date_updated":"2026-02-16T11:57:00Z","status":"public","page":"1-21","ec_funded":1,"quality_controlled":"1","type":"conference","external_id":{"arxiv":["2507.20711"]},"_id":"21090","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Fairness in AI is traditionally studied as a static property evaluated once, over a fixed dataset. However, real-world AI systems operate sequentially, with outcomes and environments evolving over time. This paper proposes a framework for analysing fairness as a runtime property. Using a minimal yet expressive model based on sequences of coin tosses with possibly evolving biases, we study the problems of monitoring and enforcing fairness expressed in either toss outcomes or coin biases. Since there is no one-size-fits-all solution for either problem, we provide a summary of monitoring and enforcement strategies, parametrised by environment dynamics, prediction horizon, and confidence thresholds. For both problems, we present general results under simple or minimal assumptions. We survey existing solutions for the monitoring problem for Markovian and additive dynamics, and existing solutions for the enforcement problem in static settings with known dynamics."}],"day":"13","citation":{"chicago":"Cano Cordoba, Filip, Thomas A Henzinger, and Konstantin Kueffner. “Algorithmic Fairness: A Runtime Perspective.” In <i>25th International Conference on Runtime Verification</i>, 16087:1–21. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_1\">https://doi.org/10.1007/978-3-032-05435-7_1</a>.","ista":"Cano Cordoba F, Henzinger TA, Kueffner K. 2025. Algorithmic fairness: A runtime perspective. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 1–21.","ama":"Cano Cordoba F, Henzinger TA, Kueffner K. Algorithmic fairness: A runtime perspective. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:1-21. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_1\">10.1007/978-3-032-05435-7_1</a>","apa":"Cano Cordoba, F., Henzinger, T. A., &#38; Kueffner, K. (2025). Algorithmic fairness: A runtime perspective. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 1–21). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_1\">https://doi.org/10.1007/978-3-032-05435-7_1</a>","short":"F. Cano Cordoba, T.A. Henzinger, K. Kueffner, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 1–21.","ieee":"F. Cano Cordoba, T. A. Henzinger, and K. Kueffner, “Algorithmic fairness: A runtime perspective,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 1–21.","mla":"Cano Cordoba, Filip, et al. “Algorithmic Fairness: A Runtime Perspective.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 1–21, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_1\">10.1007/978-3-032-05435-7_1</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","intvolume":"     16087","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2507.20711"}],"OA_place":"repository","date_published":"2025-09-13T00:00:00Z"},{"article_processing_charge":"No","corr_author":"1","publisher":"Springer Nature","volume":16087,"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"full_name":"Kueffner, Konstantin","last_name":"Kueffner","orcid":"0000-0001-8974-2542","first_name":"Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515"},{"orcid":"0000-0002-4993-773X","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","first_name":"Zhengqi","full_name":"Yu, Zhengqi","last_name":"Yu"}],"month":"09","department":[{"_id":"ToHe"}],"project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"oa":1,"doi":"10.1007/978-3-032-05435-7_4","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","date_created":"2026-01-29T16:03:01Z","title":"Formal verification of neural certificates done dynamically","alternative_title":["LNCS"],"OA_type":"green","oa_version":"Preprint","publication_identifier":{"eisbn":["9783032054357"],"issn":["0302-9743"],"eissn":["1611-3349"]},"arxiv":1,"publication_status":"published","conference":{"end_date":"2025-09-19","location":"Graz, Austria","name":"RV: Runtime Verification","start_date":"2025-09-15"},"ec_funded":1,"status":"public","page":"54-72","publication":"25th International Conference on Runtime Verification","date_updated":"2026-02-16T11:53:25Z","OA_place":"repository","date_published":"2025-09-13T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2507.11987"}],"intvolume":"     16087","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","day":"13","citation":{"mla":"Henzinger, Thomas A., et al. “Formal Verification of Neural Certificates Done Dynamically.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 54–72, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">10.1007/978-3-032-05435-7_4</a>.","ieee":"T. A. Henzinger, K. Kueffner, and E. Yu, “Formal verification of neural certificates done dynamically,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 54–72.","short":"T.A. Henzinger, K. Kueffner, E. Yu, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 54–72.","apa":"Henzinger, T. A., Kueffner, K., &#38; Yu, E. (2025). Formal verification of neural certificates done dynamically. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 54–72). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">https://doi.org/10.1007/978-3-032-05435-7_4</a>","ama":"Henzinger TA, Kueffner K, Yu E. Formal verification of neural certificates done dynamically. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:54-72. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">10.1007/978-3-032-05435-7_4</a>","ista":"Henzinger TA, Kueffner K, Yu E. 2025. Formal verification of neural certificates done dynamically. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 54–72.","chicago":"Henzinger, Thomas A, Konstantin Kueffner, and Emily Yu. “Formal Verification of Neural Certificates Done Dynamically.” In <i>25th International Conference on Runtime Verification</i>, 16087:54–72. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">https://doi.org/10.1007/978-3-032-05435-7_4</a>."},"external_id":{"arxiv":["2507.11987"]},"abstract":[{"lang":"eng","text":"Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates."}],"_id":"21091","language":[{"iso":"eng"}],"quality_controlled":"1","type":"conference"},{"publication_identifier":{"eisbn":["9783032054357"],"issn":["0302-9743"],"eissn":["1611-3349"]},"arxiv":1,"oa_version":"Preprint","OA_type":"green","date_created":"2026-01-29T16:03:43Z","title":"Alignment monitoring","alternative_title":["LNCS"],"conference":{"end_date":"2025-09-19","location":"Graz, Austria","name":"RV: Runtime Verification","start_date":"2025-09-15"},"publication_status":"published","publisher":"Springer Nature","corr_author":"1","article_processing_charge":"No","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","doi":"10.1007/978-3-032-05435-7_9","oa":1,"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"department":[{"_id":"ToHe"}],"month":"09","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"orcid":"0000-0001-8974-2542","first_name":"Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","full_name":"Kueffner, Konstantin","last_name":"Kueffner"},{"full_name":"Singh, Vasu","last_name":"Singh","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87"},{"first_name":"I","last_name":"Sun","full_name":"Sun, I"}],"volume":16087,"year":"2025","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"     16087","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2508.00021"}],"date_published":"2025-09-13T00:00:00Z","OA_place":"repository","type":"conference","quality_controlled":"1","abstract":[{"text":"Formal verification provides assurances that a probabilistic system satisfies its specification—conditioned on the system model being aligned with reality. We propose alignment monitoring to watch that this assumption is justified. We consider a probabilistic model well aligned if it accurately predicts the behaviour of an uncertain system in advance. An alignment score measures this by quantifying the similarity between the model’s predicted and the system’s (unknown) actual distributions. An alignment monitor observes the system at runtime; at each point in time it uses the current state and the model to predict the next state. After the next state is observed, the monitor updates the verdict, which is a high-probability interval estimate for the true alignment score. We utilize tools from sequential forecasting to construct our alignment monitors. Besides a monitor for measuring the expected alignment score, we introduce a differential alignment monitor, designed for comparing two models, and a weighted alignment monitor, which permits task-specific alignment monitoring. We evaluate our monitors experimentally on the PRISM benchmark suite. They are fast, memory-efficient, and detect misalignment early.","lang":"eng"}],"_id":"21092","language":[{"iso":"eng"}],"external_id":{"arxiv":["2508.00021"]},"citation":{"ista":"Henzinger TA, Kueffner K, Singh V, Sun I. 2025. Alignment monitoring. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 140–159.","ama":"Henzinger TA, Kueffner K, Singh V, Sun I. Alignment monitoring. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:140-159. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_9\">10.1007/978-3-032-05435-7_9</a>","chicago":"Henzinger, Thomas A, Konstantin Kueffner, Vasu Singh, and I Sun. “Alignment Monitoring.” In <i>25th International Conference on Runtime Verification</i>, 16087:140–59. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_9\">https://doi.org/10.1007/978-3-032-05435-7_9</a>.","short":"T.A. Henzinger, K. Kueffner, V. Singh, I. Sun, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 140–159.","ieee":"T. A. Henzinger, K. Kueffner, V. Singh, and I. Sun, “Alignment monitoring,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 140–159.","mla":"Henzinger, Thomas A., et al. “Alignment Monitoring.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 140–59, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_9\">10.1007/978-3-032-05435-7_9</a>.","apa":"Henzinger, T. A., Kueffner, K., Singh, V., &#38; Sun, I. (2025). Alignment monitoring. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 140–159). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_9\">https://doi.org/10.1007/978-3-032-05435-7_9</a>"},"day":"13","page":"140-159","status":"public","ec_funded":1,"publication":"25th International Conference on Runtime Verification","date_updated":"2026-02-16T11:56:38Z"},{"quality_controlled":"1","type":"conference","external_id":{"arxiv":["2508.02301"]},"_id":"21093","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"We propose a monitoring approach for hyperproperties where the system’s observations range over infinite domains. The specifications are given as formulas of symbolic hypernode logic, an extension of earlier versions of hypernode logic that supports events with data. We demonstrate how to translate terms of symbolic hypernode logic into multi-tape symbolic transducers and we present a monitoring algorithm for universally quantified formulas that is based on this translation. We evaluate our approach against the previous approach for monitoring hypernode logic, and we also compare it to other monitors for hyperproperties."}],"day":"13","citation":{"mla":"Chalupa, Marek, et al. “Monitoring Hypernode Logic over Infinite Domains.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 417–37, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">10.1007/978-3-032-05435-7_23</a>.","ieee":"M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Monitoring hypernode logic over infinite domains,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 417–437.","short":"M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 417–437.","apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. A. (2025). Monitoring hypernode logic over infinite domains. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 417–437). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">https://doi.org/10.1007/978-3-032-05435-7_23</a>","ama":"Chalupa M, Henzinger TA, Oliveira da Costa AA. Monitoring hypernode logic over infinite domains. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:417-437. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">10.1007/978-3-032-05435-7_23</a>","ista":"Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Monitoring hypernode logic over infinite domains. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 417–437.","chicago":"Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Monitoring Hypernode Logic over Infinite Domains.” In <i>25th International Conference on Runtime Verification</i>, 16087:417–37. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">https://doi.org/10.1007/978-3-032-05435-7_23</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","intvolume":"     16087","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2508.02301","open_access":"1"}],"OA_place":"repository","date_published":"2025-09-13T00:00:00Z","publication":"25th International Conference on Runtime Verification","date_updated":"2026-02-16T11:59:20Z","status":"public","page":"417-437","ec_funded":1,"conference":{"name":"RV: Runtime Verification","start_date":"2025-09-15","end_date":"2025-09-19","location":"Graz, Austria"},"publication_status":"published","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783032054357"]},"arxiv":1,"OA_type":"green","oa_version":"Preprint","title":"Monitoring hypernode logic over infinite domains","date_created":"2026-01-29T16:04:31Z","alternative_title":["LNCS"],"oa":1,"doi":"10.1007/978-3-032-05435-7_23","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 and in part by the FWF-2022-SFB F8502 (SPyCoDe).","department":[{"_id":"ToHe"}],"month":"09","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"}],"author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"first_name":"Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","full_name":"Oliveira da Costa, Ana A","last_name":"Oliveira da Costa"}],"volume":16087,"publisher":"Springer Nature","article_processing_charge":"No","corr_author":"1"},{"citation":{"ama":"Auerbach B, Cueto Noval M, Erol B, Pietrzak KZ. Continuous group-key agreement: Concurrent updates without pruning. In: <i>45th Annual International Cryptology Conference</i>. Vol 16007. Springer Nature; 2025:141-172. doi:<a href=\"https://doi.org/10.1007/978-3-032-01913-4_5\">10.1007/978-3-032-01913-4_5</a>","ista":"Auerbach B, Cueto Noval M, Erol B, Pietrzak KZ. 2025. Continuous group-key agreement: Concurrent updates without pruning. 45th Annual International Cryptology Conference. CRYPTO: International Cryptology Conference, LNCS, vol. 16007, 141–172.","chicago":"Auerbach, Benedikt, Miguel Cueto Noval, Boran Erol, and Krzysztof Z Pietrzak. “Continuous Group-Key Agreement: Concurrent Updates without Pruning.” In <i>45th Annual International Cryptology Conference</i>, 16007:141–72. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-01913-4_5\">https://doi.org/10.1007/978-3-032-01913-4_5</a>.","mla":"Auerbach, Benedikt, et al. “Continuous Group-Key Agreement: Concurrent Updates without Pruning.” <i>45th Annual International Cryptology Conference</i>, vol. 16007, Springer Nature, 2025, pp. 141–72, doi:<a href=\"https://doi.org/10.1007/978-3-032-01913-4_5\">10.1007/978-3-032-01913-4_5</a>.","ieee":"B. Auerbach, M. Cueto Noval, B. Erol, and K. Z. Pietrzak, “Continuous group-key agreement: Concurrent updates without pruning,” in <i>45th Annual International Cryptology Conference</i>, Santa Barbara, CA, United States, 2025, vol. 16007, pp. 141–172.","short":"B. Auerbach, M. Cueto Noval, B. Erol, K.Z. Pietrzak, in:, 45th Annual International Cryptology Conference, Springer Nature, 2025, pp. 141–172.","apa":"Auerbach, B., Cueto Noval, M., Erol, B., &#38; Pietrzak, K. Z. (2025). Continuous group-key agreement: Concurrent updates without pruning. In <i>45th Annual International Cryptology Conference</i> (Vol. 16007, pp. 141–172). Santa Barbara, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-01913-4_5\">https://doi.org/10.1007/978-3-032-01913-4_5</a>"},"day":"17","quality_controlled":"1","type":"conference","_id":"21262","abstract":[{"lang":"eng","text":"Continuous Group Key Agreement (CGKA) is the primitive underlying secure group messaging. It allows a large group of N users to maintain a shared secret key that is frequently rotated by the\r\ngroup members in order to achieve forward secrecy and post compromise security. The group messaging scheme Messaging Layer Security (MLS) standardized by the IETF makes use of a CGKA called TreeKEM which arranges the N group members in a binary tree. Here, each node is associated with a public-key, each user is assigned one of the leaves, and a user knows the corresponding secret keys from their leaf to the root. To update the key material known to them, a user must just replace keys at log(N) nodes, which requires them to create and upload log(N) ciphertexts. Such updates must be processed sequentially by all users, which for large groups is impractical. To allow for concurrent updates, TreeKEM uses the “propose and commit” paradigm, where multiple users can concurrently propose to update (by just sampling a fresh leaf key), and a single user can then commit to all proposals at once. Unfortunately, this process destroys the binary tree structure as the tree gets pruned and some nodes must be “blanked” at the cost of increasing the in-degree of others, which makes the commit operation, as well as, future commits more costly. In the worst case, the update cost (in terms of uploaded ciphertexts) per user can grow from log(N) to Ω(N). In this work we provide two main contributions. First, we show that MLS’ communication complexity is bad not only in the worst case but also if the proposers and committers are chosen at random: even if there’s just one update proposal for every commit the expected cost is already over √N, and it approaches N as this ratio changes towards more proposals. Our second contribution is a new variant of propose and commit for\r\nTreeKEM which for moderate amounts of update proposals per commit provably achieves an update cost of Θ(log(N)) assuming the proposers and committers are chosen at random."}],"language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2025/1035"}],"OA_place":"repository","date_published":"2025-08-17T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","intvolume":"     16007","publication":"45th Annual International Cryptology Conference","date_updated":"2026-02-18T07:36:42Z","status":"public","page":"141-172","conference":{"start_date":"2025-08-17","name":"CRYPTO: International Cryptology Conference","location":"Santa Barbara, CA, United States","end_date":"2025-08-21"},"publication_status":"published","OA_type":"green","oa_version":"Preprint","date_created":"2026-02-17T07:41:04Z","alternative_title":["LNCS"],"title":"Continuous group-key agreement: Concurrent updates without pruning","publication_identifier":{"isbn":["9783032019127"],"eisbn":["9783032019134"],"issn":["0302-9743"],"eissn":["1611-3349"]},"month":"08","department":[{"_id":"KrPi"}],"author":[{"orcid":"0000-0002-7553-6606","id":"D33D2B18-E445-11E9-ABB7-15F4E5697425","first_name":"Benedikt","last_name":"Auerbach","full_name":"Auerbach, Benedikt"},{"last_name":"Cueto Noval","full_name":"Cueto Noval, Miguel","orcid":"0000-0002-2505-4246","first_name":"Miguel","id":"ffc563a3-f6e0-11ea-865d-e3cce03d17cc"},{"full_name":"Erol, Boran","last_name":"Erol","first_name":"Boran"},{"first_name":"Krzysztof Z","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9139-1654","last_name":"Pietrzak","full_name":"Pietrzak, Krzysztof Z"}],"volume":16007,"oa":1,"doi":"10.1007/978-3-032-01913-4_5","acknowledgement":"B. Auerbach and B. Erol—Conducted part of this work at ISTA.","publisher":"Springer Nature","article_processing_charge":"No"},{"page":"584-616","status":"public","publication":"45th Annual International Cryptology Conference","date_updated":"2026-02-19T07:50:33Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","intvolume":"     16005","main_file_link":[{"url":"https://eprint.iacr.org/2025/514","open_access":"1"}],"OA_place":"repository","date_published":"2025-08-17T00:00:00Z","quality_controlled":"1","type":"conference","language":[{"iso":"eng"}],"_id":"21323","abstract":[{"lang":"eng","text":"We present a unifying framework for proving the knowledge-soundness of KZG-like polynomial commitment schemes, encompassing both univariate and multivariate variants. By conceptualizing the proof technique of Lipmaa, Parisella, and Siim for the univariate KZG scheme (EUROCRYPT 2024), we present tools and falsifiable hardness assumptions that permit black-box extraction of the multivariate KZG scheme. Central to our approach is the notion of a canonical Proof-of-Knowledge of a Polynomial (PoKoP) of a polynomial commitment scheme, which we use to capture the extractability notion required in constructions of practical zk-SNARKs. We further present an explicit polynomial decomposition lemma for multivariate polynomials, enabling a more direct analysis of interpolating extractors and bridging the gap between univariate and multivariate commitments. Our results provide the first standard-model proofs of extractability for the multivariate KZG scheme and many of its variants under falsifiable assumptions."}],"citation":{"chicago":"Belohorec, Juraj, Pavel Dvořák, Charlotte Hoffmann, Pavel Hubáček, Kristýna Mašková, and Martin Pastyřík. “On Extractability of the KZG Family of Polynomial Commitment Schemes.” In <i>45th Annual International Cryptology Conference</i>, 16005:584–616. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-01887-8_19\">https://doi.org/10.1007/978-3-032-01887-8_19</a>.","ama":"Belohorec J, Dvořák P, Hoffmann C, Hubáček P, Mašková K, Pastyřík M. On extractability of the KZG family of polynomial commitment schemes. In: <i>45th Annual International Cryptology Conference</i>. Vol 16005. Springer Nature; 2025:584-616. doi:<a href=\"https://doi.org/10.1007/978-3-032-01887-8_19\">10.1007/978-3-032-01887-8_19</a>","ista":"Belohorec J, Dvořák P, Hoffmann C, Hubáček P, Mašková K, Pastyřík M. 2025. On extractability of the KZG family of polynomial commitment schemes. 45th Annual International Cryptology Conference. CRYPTO: International Cryptology Conference, LNCS, vol. 16005, 584–616.","apa":"Belohorec, J., Dvořák, P., Hoffmann, C., Hubáček, P., Mašková, K., &#38; Pastyřík, M. (2025). On extractability of the KZG family of polynomial commitment schemes. In <i>45th Annual International Cryptology Conference</i> (Vol. 16005, pp. 584–616). Santa Barbara, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-01887-8_19\">https://doi.org/10.1007/978-3-032-01887-8_19</a>","mla":"Belohorec, Juraj, et al. “On Extractability of the KZG Family of Polynomial Commitment Schemes.” <i>45th Annual International Cryptology Conference</i>, vol. 16005, Springer Nature, 2025, pp. 584–616, doi:<a href=\"https://doi.org/10.1007/978-3-032-01887-8_19\">10.1007/978-3-032-01887-8_19</a>.","short":"J. Belohorec, P. Dvořák, C. Hoffmann, P. Hubáček, K. Mašková, M. Pastyřík, in:, 45th Annual International Cryptology Conference, Springer Nature, 2025, pp. 584–616.","ieee":"J. Belohorec, P. Dvořák, C. Hoffmann, P. Hubáček, K. Mašková, and M. Pastyřík, “On extractability of the KZG family of polynomial commitment schemes,” in <i>45th Annual International Cryptology Conference</i>, Santa Barbara, CA, United States, 2025, vol. 16005, pp. 584–616."},"day":"17","publisher":"Springer Nature","article_processing_charge":"No","oa":1,"doi":"10.1007/978-3-032-01887-8_19","acknowledgement":"Juraj Belohorec, Pavel Hubáček, and Kristýna Mašková were partially supported by the Academy of Sciences of the Czech Republic (RVO 67985840), Czech Science Foundation GAČR grant No. 25-16311S, and by Zircuit. Pavel Dvořák was supported by Czech Science Foundation GAČR grant No. 22-14872O. Juraj Belohorec and Kristýna Mašková were supported by the grant SVV–2025–260822.","department":[{"_id":"KrPi"}],"month":"08","volume":16005,"author":[{"first_name":"Juraj","last_name":"Belohorec","full_name":"Belohorec, Juraj"},{"first_name":"Pavel","last_name":"Dvořák","full_name":"Dvořák, Pavel"},{"last_name":"Hoffmann","full_name":"Hoffmann, Charlotte","first_name":"Charlotte","id":"0f78d746-dc7d-11ea-9b2f-83f92091afe7","orcid":"0000-0003-2027-5549"},{"full_name":"Hubáček, Pavel","last_name":"Hubáček","first_name":"Pavel"},{"full_name":"Mašková, Kristýna","last_name":"Mašková","first_name":"Kristýna"},{"first_name":"Martin","last_name":"Pastyřík","full_name":"Pastyřík, Martin"}],"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783032018878"],"isbn":["9783032018861"]},"OA_type":"green","oa_version":"Preprint","alternative_title":["LNCS"],"date_created":"2026-02-18T10:59:58Z","title":"On extractability of the KZG family of polynomial commitment schemes","conference":{"end_date":"2025-08-221","location":"Santa Barbara, CA, United States","name":"CRYPTO: International Cryptology Conference","start_date":"2025-08-17"},"publication_status":"published"},{"OA_place":"publisher","date_published":"2025-05-01T00:00:00Z","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2025","intvolume":"     15696","day":"01","citation":{"ista":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2025. Automating the analysis of quantitative automata with QuAK. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 15696, 303–312.","ama":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. Automating the analysis of quantitative automata with QuAK. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer Nature; 2025:303-312. doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">10.1007/978-3-031-90643-5_16</a>","chicago":"Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Automating the Analysis of Quantitative Automata with QuAK.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:303–12. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">https://doi.org/10.1007/978-3-031-90643-5_16</a>.","short":"M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 303–312.","ieee":"M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Automating the analysis of quantitative automata with QuAK,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 2025, vol. 15696, pp. 303–312.","mla":"Chalupa, Marek, et al. “Automating the Analysis of Quantitative Automata with QuAK.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 303–12, doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">10.1007/978-3-031-90643-5_16</a>.","apa":"Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2025). Automating the analysis of quantitative automata with QuAK. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 303–312). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">https://doi.org/10.1007/978-3-031-90643-5_16</a>"},"has_accepted_license":"1","quality_controlled":"1","type":"conference","external_id":{"arxiv":["2501.16088"]},"abstract":[{"lang":"eng","text":"Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize acceptance conditions of boolean w-automata. Despite the theoretical advances in systems analysis through quantitative automata, the first comprehensive software tool for quantitative automata (Quantitative Automata Kit, or QuAK) was developed only recently. QuAK implements algorithms for solving standard decision problems, e.g., emptiness and universality, as well as constructions for safety and liveness of quantitative automata. We present the architecture of QuAK, which reflects that all of these problems reduce to either checking inclusion between two quantitative automata or computing the highest value achievable by an automaton—its so-called top value. We improve QuAK by extending these two algorithms with an option to return, alongside their results, an ultimately periodic word witnessing the algorithm’s output, as well as implementing a new safety-liveness decomposition algorithm that can handle nondeterministic automata, making QuAK more informative and capable."}],"_id":"19741","language":[{"iso":"eng"}],"scopus_import":"1","ec_funded":1,"page":"303-312","status":"public","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","date_updated":"2026-04-07T12:02:57Z","file_date_updated":"2025-06-02T08:13:11Z","OA_type":"hybrid","oa_version":"Published Version","title":"Automating the analysis of quantitative automata with QuAK","date_created":"2025-05-25T22:17:07Z","alternative_title":["LNCS"],"publication_identifier":{"isbn":["9783031906428"],"issn":["0302-9743"],"eissn":["1611-3349"]},"arxiv":1,"file":[{"file_id":"19768","date_updated":"2025-06-02T08:13:11Z","creator":"dernst","relation":"main_file","file_name":"2025_TACAS_ChalupaMarek.pdf","checksum":"a27fa245be8d83421e9127b48a09c8af","date_created":"2025-06-02T08:13:11Z","file_size":420669,"success":1,"content_type":"application/pdf","access_level":"open_access"}],"publication_status":"published","related_material":{"record":[{"id":"20147","status":"public","relation":"dissertation_contains"}]},"publisher":"Springer Nature","article_processing_charge":"No","tmp":{"short":"CC BY (4.0)","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)"},"corr_author":"1","department":[{"_id":"ToHe"}],"month":"05","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"volume":15696,"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien"},{"last_name":"Sarac","full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E"}],"oa":1,"doi":"10.1007/978-3-031-90643-5_16","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093."},{"date_updated":"2026-04-16T09:11:09Z","publication":"28th IACR International Conference on Practice and Theory of Public-Key Cryptography","page":"36-66","status":"public","scopus_import":"1","_id":"19778","abstract":[{"lang":"eng","text":"A verifiable delay function VDF(x, T)->(y, π) maps an input x and time parameter T to an output y together with an efficiently verifiable proof π certifying that y was correctly computed. The function runs in T sequential steps, and it should not be possible to compute y much faster than that. The only known practical VDFs use sequential squaring in groups of unknown order as the sequential function, i.e., y = x^2^T. There are two constructions for the proof of exponentiation (PoE) certifying that y = x^2^T, with Wesolowski (Eurocrypt’19) having very short proofs, but they are more expensive to compute and the soundness relies on stronger assumptions than the PoE proposed by Pietrzak (ITCS’19).\r\nA recent application of VDFs by Arun, Bonneau and Clark (Asiacrypt’22) are short-lived proofs and signatures, which are proofs and signatures that are only sound for some time t, but after that can be forged by anyone. For this they rely on “watermarkable VDFs”, where the proof embeds a prover chosen watermark. To achieve stronger notions of proofs/signatures with reusable forgeability, they rely on “zero-knowledge VDFs”, where instead of the output y, one just proves knowledge of this output. The existing proposals for watermarkable and zero-knowledge VDFs all build on Wesolowski’s PoE, for the watermarkable VDFs there’s currently no security proof.\r\n\r\nIn this work we give the first constructions that transform any PoEs in hidden order groups into watermarkable VDFs and into zkVDFs, solving an open question by Arun et al. Unlike our watermarkable VDF, the zkVDF (required for reusable forgeability) is not very practical as the number of group elements in the proof is a security parameter. To address this, we introduce the notion of zero-knowledge proofs of sequential work (zkPoSW), a notion that relaxes zkVDFs by not requiring that the output is unique. We show that zkPoSW are sufficient to construct proofs or signatures with reusable forgeability, and construct efficient zkPoSW from any PoE, ultimately achieving short lived proofs and signatures that improve upon Arun et al.’s construction in several dimensions (faster forging times, arguably weaker assumptions).\r\nA key idea underlying our constructions is to not directly construct a (watermarked or zk) proof for y = x^2^T, but instead give a (watermarked or zk) proof for the more basic statement that \r\nx^l, y^l satisfy x^l = x ^r, y^l = y^r for some r, together with a normal PoE for y^l = (x^l)^2^T."}],"language":[{"iso":"eng"}],"quality_controlled":"1","type":"conference","day":"01","citation":{"apa":"Hoffmann, C., &#38; Pietrzak, K. Z. (2025). Watermarkable and zero-knowledge Verifiable Delay Functions from any proof of exponentiation. In <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i> (Vol. 15674, pp. 36–66). Roros, Norway: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-91820-9_2\">https://doi.org/10.1007/978-3-031-91820-9_2</a>","short":"C. Hoffmann, K.Z. Pietrzak, in:, 28th IACR International Conference on Practice and Theory of Public-Key Cryptography, Springer Nature, 2025, pp. 36–66.","ieee":"C. Hoffmann and K. Z. Pietrzak, “Watermarkable and zero-knowledge Verifiable Delay Functions from any proof of exponentiation,” in <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i>, Roros, Norway, 2025, vol. 15674, pp. 36–66.","mla":"Hoffmann, Charlotte, and Krzysztof Z. Pietrzak. “Watermarkable and Zero-Knowledge Verifiable Delay Functions from Any Proof of Exponentiation.” <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i>, vol. 15674, Springer Nature, 2025, pp. 36–66, doi:<a href=\"https://doi.org/10.1007/978-3-031-91820-9_2\">10.1007/978-3-031-91820-9_2</a>.","chicago":"Hoffmann, Charlotte, and Krzysztof Z Pietrzak. “Watermarkable and Zero-Knowledge Verifiable Delay Functions from Any Proof of Exponentiation.” In <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i>, 15674:36–66. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-91820-9_2\">https://doi.org/10.1007/978-3-031-91820-9_2</a>.","ista":"Hoffmann C, Pietrzak KZ. 2025. Watermarkable and zero-knowledge Verifiable Delay Functions from any proof of exponentiation. 28th IACR International Conference on Practice and Theory of Public-Key Cryptography. PKC: Public-Key Cryptography, LNCS, vol. 15674, 36–66.","ama":"Hoffmann C, Pietrzak KZ. Watermarkable and zero-knowledge Verifiable Delay Functions from any proof of exponentiation. In: <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i>. Vol 15674. Springer Nature; 2025:36-66. doi:<a href=\"https://doi.org/10.1007/978-3-031-91820-9_2\">10.1007/978-3-031-91820-9_2</a>"},"intvolume":"     15674","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","year":"2025","OA_place":"repository","date_published":"2025-01-01T00:00:00Z","main_file_link":[{"url":"https://ia.cr/2024/481","open_access":"1"}],"doi":"10.1007/978-3-031-91820-9_2","oa":1,"author":[{"last_name":"Hoffmann","full_name":"Hoffmann, Charlotte","orcid":"0000-0003-2027-5549","id":"0f78d746-dc7d-11ea-9b2f-83f92091afe7","first_name":"Charlotte"},{"id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","first_name":"Krzysztof Z","orcid":"0000-0002-9139-1654","last_name":"Pietrzak","full_name":"Pietrzak, Krzysztof Z"}],"volume":15674,"month":"01","department":[{"_id":"KrPi"},{"_id":"GradSch"}],"article_processing_charge":"No","corr_author":"1","publisher":"Springer Nature","related_material":{"record":[{"status":"public","id":"20920","relation":"dissertation_contains"},{"relation":"dissertation_contains","status":"public","id":"20556"}]},"conference":{"name":"PKC: Public-Key Cryptography","start_date":"2025-05-12","end_date":"2025-05-15","location":"Roros, Norway"},"publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031918209"],"isbn":["9783031918193"]},"title":"Watermarkable and zero-knowledge Verifiable Delay Functions from any proof of exponentiation","date_created":"2025-06-03T07:30:21Z","alternative_title":["LNCS"],"OA_type":"green","oa_version":"Preprint"},{"conference":{"name":"FM: Formal Methods","start_date":"2024-09-09","end_date":"2024-09-13","location":"Milan, Italy"},"publication_status":"published","file":[{"success":1,"content_type":"application/pdf","date_created":"2024-10-01T09:56:54Z","file_size":650495,"access_level":"open_access","creator":"dernst","relation":"main_file","date_updated":"2024-10-01T09:56:54Z","file_id":"18165","checksum":"223845be9e754681ee218866827c95e7","file_name":"2024_LNCS_Chatterjee.pdf"}],"arxiv":1,"publication_identifier":{"isbn":["9783031711619"],"eissn":["1611-3349"],"issn":["0302-9743"]},"alternative_title":["LNCS"],"title":"Sound and complete witnesses for template-based verification of LTL properties on polynomial programs","date_created":"2024-09-29T22:01:37Z","oa_version":"Published Version","oa":1,"doi":"10.1007/978-3-031-71162-6_31","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.","volume":14933,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584"},{"first_name":"Ehsan","full_name":"Goharshady, Ehsan","last_name":"Goharshady"},{"last_name":"Karrabi","full_name":"Karrabi, Mehrdad","first_name":"Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","last_name":"Zikelic","full_name":"Zikelic, Dorde"}],"department":[{"_id":"KrCh"}],"month":"09","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818"}],"article_processing_charge":"Yes (in subscription journal)","tmp":{"short":"CC BY (4.0)","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)"},"corr_author":"1","publisher":"Springer Nature","external_id":{"isi":["001336893300031"],"arxiv":["2403.05386"]},"_id":"18155","abstract":[{"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.","lang":"eng"}],"language":[{"iso":"eng"}],"quality_controlled":"1","type":"conference","day":"11","citation":{"apa":"Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., &#38; Zikelic, D. (2024). Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 14933, pp. 600–619). Milan, Italy: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">https://doi.org/10.1007/978-3-031-71162-6_31</a>","mla":"Chatterjee, Krishnendu, et al. “Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 14933, Springer Nature, 2024, pp. 600–19, doi:<a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">10.1007/978-3-031-71162-6_31</a>.","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.","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 <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Milan, Italy, 2024, vol. 14933, pp. 600–619.","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 <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, 14933:600–619. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">https://doi.org/10.1007/978-3-031-71162-6_31</a>.","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: <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 14933. Springer Nature; 2024:600-619. doi:<a href=\"https://doi.org/10.1007/978-3-031-71162-6_31\">10.1007/978-3-031-71162-6_31</a>","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."},"has_accepted_license":"1","intvolume":"     14933","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ddc":["000"],"year":"2024","date_published":"2024-09-11T00:00:00Z","file_date_updated":"2024-10-01T09:56:54Z","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","date_updated":"2025-09-08T09:51:34Z","isi":1,"page":"600-619","status":"public","ec_funded":1,"scopus_import":"1"},{"day":"19","citation":{"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.","ama":"Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. BNClassifier: Classifying boolean models by dynamic properties. In: <i>Computational Methods in Systems Biology</i>. Vol 14971. Springer Nature; 2024:19-26. doi:<a href=\"https://doi.org/10.1007/978-3-031-71671-3_2\">10.1007/978-3-031-71671-3_2</a>","chicago":"Beneš, Nikola, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek. “BNClassifier: Classifying Boolean Models by Dynamic Properties.” In <i>Computational Methods in Systems Biology</i>, 14971:19–26. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-71671-3_2\">https://doi.org/10.1007/978-3-031-71671-3_2</a>.","ieee":"N. Beneš, L. Brim, O. Huvar, S. Pastva, and D. Šafránek, “BNClassifier: Classifying boolean models by dynamic properties,” in <i>Computational Methods in Systems Biology</i>, 2024, vol. 14971, pp. 19–26.","short":"N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, in:, Computational Methods in Systems Biology, Springer Nature, 2024, pp. 19–26.","mla":"Beneš, Nikola, et al. “BNClassifier: Classifying Boolean Models by Dynamic Properties.” <i>Computational Methods in Systems Biology</i>, vol. 14971, Springer Nature, 2024, pp. 19–26, doi:<a href=\"https://doi.org/10.1007/978-3-031-71671-3_2\">10.1007/978-3-031-71671-3_2</a>.","apa":"Beneš, N., Brim, L., Huvar, O., Pastva, S., &#38; Šafránek, D. (2024). BNClassifier: Classifying boolean models by dynamic properties. In <i>Computational Methods in Systems Biology</i> (Vol. 14971, pp. 19–26). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-71671-3_2\">https://doi.org/10.1007/978-3-031-71671-3_2</a>"},"external_id":{"isi":["001333144400002"]},"_id":"18177","language":[{"iso":"eng"}],"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."}],"quality_controlled":"1","type":"conference","date_published":"2024-09-19T00:00:00Z","intvolume":"     14971","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2024","date_updated":"2025-09-08T09:54:27Z","publication":"Computational Methods in Systems Biology","isi":1,"ec_funded":1,"scopus_import":"1","page":"19-26","status":"public","publication_status":"published","alternative_title":["LNBI"],"title":"BNClassifier: Classifying boolean models by dynamic properties","date_created":"2024-10-06T22:01:12Z","oa_version":"None","publication_identifier":{"isbn":["9783031716706"],"eissn":["1611-3349"],"issn":["0302-9743"]},"volume":14971,"author":[{"last_name":"Beneš","full_name":"Beneš, Nikola","first_name":"Nikola"},{"last_name":"Brim","full_name":"Brim, Luboš","first_name":"Luboš"},{"first_name":"Ondřej","last_name":"Huvar","full_name":"Huvar, Ondřej"},{"last_name":"Pastva","full_name":"Pastva, Samuel","orcid":"0000-0003-1993-0331","first_name":"Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b"},{"first_name":"David","full_name":"Šafránek, David","last_name":"Šafránek"}],"month":"09","department":[{"_id":"ToHe"}],"project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program"}],"doi":"10.1007/978-3-031-71671-3_2","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.","article_processing_charge":"No","publisher":"Springer Nature"},{"scopus_import":"1","extern":"1","publisher":"Springer Nature","status":"public","page":"160-171","article_processing_charge":"No","month":"08","publication":"First International Conference on Artificial Intelligence in Healthcare","date_updated":"2024-10-09T10:33:39Z","volume":14976,"author":[{"full_name":"Rave, Gilad","last_name":"Rave","first_name":"Gilad"},{"first_name":"Daniel E.","last_name":"Fordham","full_name":"Fordham, Daniel E."},{"last_name":"Bronstein","full_name":"Bronstein, Alexander","orcid":"0000-0001-9699-8730","id":"58f3726e-7cba-11ef-ad8b-e6e8cb3904e6","first_name":"Alexander"},{"full_name":"Silver, David H.","last_name":"Silver","first_name":"David H."}],"doi":"10.1007/978-3-031-67285-9_12","oa_version":"None","date_published":"2024-08-15T00:00:00Z","title":"Enhancing predictive accuracy in embryo implantation: The Bonna algorithm and its clinical implications","alternative_title":["LNCS"],"date_created":"2024-10-08T12:46:23Z","year":"2024","publication_identifier":{"isbn":["9783031672842"],"eisbn":["9783031672859"],"eissn":["1611-3349"],"issn":["0302-9743"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"     14976","citation":{"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 <i>First International Conference on Artificial Intelligence in Healthcare</i>, 14976:160–71. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-67285-9_12\">https://doi.org/10.1007/978-3-031-67285-9_12</a>.","ama":"Rave G, Fordham DE, Bronstein AM, Silver DH. Enhancing predictive accuracy in embryo implantation: The Bonna algorithm and its clinical implications. In: <i>First International Conference on Artificial Intelligence in Healthcare</i>. Vol 14976. Springer Nature; 2024:160-171. doi:<a href=\"https://doi.org/10.1007/978-3-031-67285-9_12\">10.1007/978-3-031-67285-9_12</a>","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.","apa":"Rave, G., Fordham, D. E., Bronstein, A. M., &#38; Silver, D. H. (2024). Enhancing predictive accuracy in embryo implantation: The Bonna algorithm and its clinical implications. In <i>First International Conference on Artificial Intelligence in Healthcare</i> (Vol. 14976, pp. 160–171). Swansea, United Kingdom: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-67285-9_12\">https://doi.org/10.1007/978-3-031-67285-9_12</a>","mla":"Rave, Gilad, et al. “Enhancing Predictive Accuracy in Embryo Implantation: The Bonna Algorithm and Its Clinical Implications.” <i>First International Conference on Artificial Intelligence in Healthcare</i>, vol. 14976, Springer Nature, 2024, pp. 160–71, doi:<a href=\"https://doi.org/10.1007/978-3-031-67285-9_12\">10.1007/978-3-031-67285-9_12</a>.","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 <i>First International Conference on Artificial Intelligence in Healthcare</i>, Swansea, United Kingdom, 2024, vol. 14976, pp. 160–171.","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."},"day":"15","type":"conference","quality_controlled":"1","publication_status":"published","conference":{"location":"Swansea, United Kingdom","end_date":"2024-09-06","start_date":"2024-09-04","name":"AIiH: Artificial Intelligence in Healthcare"},"_id":"18206","language":[{"iso":"eng"}],"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."}]},{"quality_controlled":"1","type":"conference","external_id":{"arxiv":["2408.05033"],"isi":["001420093700018"]},"language":[{"iso":"eng"}],"_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."}],"citation":{"apa":"Bonakdarpour, B., Momtaz, A., Nickovic, D., &#38; Sarac, N. E. (2024). Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. In <i>24th International Conference on Runtime Verification</i> (Vol. 15191, pp. 282–301). Istanbul, Turkey: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">https://doi.org/10.1007/978-3-031-74234-7_18</a>","short":"B. Bonakdarpour, A. Momtaz, D. Nickovic, N.E. Sarac, in:, 24th International Conference on Runtime Verification, Springer Nature, 2024, pp. 282–301.","ieee":"B. Bonakdarpour, A. Momtaz, D. Nickovic, and N. E. Sarac, “Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy,” in <i>24th International Conference on Runtime Verification</i>, Istanbul, Turkey, 2024, vol. 15191, pp. 282–301.","mla":"Bonakdarpour, Borzoo, et al. “Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed &#38; Accuracy.” <i>24th International Conference on Runtime Verification</i>, vol. 15191, Springer Nature, 2024, pp. 282–301, doi:<a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">10.1007/978-3-031-74234-7_18</a>.","chicago":"Bonakdarpour, Borzoo, Anik Momtaz, Dejan Nickovic, and Naci E Sarac. “Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed &#38; Accuracy.” In <i>24th International Conference on Runtime Verification</i>, 15191:282–301. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">https://doi.org/10.1007/978-3-031-74234-7_18</a>.","ista":"Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. 2024. Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. 24th International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 15191, 282–301.","ama":"Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. Approximate distributed monitoring under partial synchrony: Balancing speed &#38; accuracy. In: <i>24th International Conference on Runtime Verification</i>. Vol 15191. Springer Nature; 2024:282-301. doi:<a href=\"https://doi.org/10.1007/978-3-031-74234-7_18\">10.1007/978-3-031-74234-7_18</a>"},"day":"12","has_accepted_license":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ddc":["000"],"year":"2024","intvolume":"     15191","OA_place":"publisher","date_published":"2024-10-12T00:00:00Z","APC_amount":"2290 EUR","file_date_updated":"2024-11-11T09:42:28Z","isi":1,"publication":"24th International Conference on Runtime Verification","date_updated":"2025-09-08T14:39:14Z","page":"282-301","status":"public","scopus_import":"1","ec_funded":1,"publication_status":"published","conference":{"start_date":"2024-10-15","name":"RV: Conference on Runtime Verification","location":"Istanbul, Turkey","end_date":"2024-10-17"},"file":[{"relation":"main_file","date_updated":"2024-11-11T09:42:28Z","file_id":"18539","creator":"dernst","file_name":"2024_LNCS_Bonakdarpour.pdf","checksum":"7b8ca21b8c19ab796fa445b0e54003ca","date_created":"2024-11-11T09:42:28Z","file_size":1897101,"content_type":"application/pdf","success":1,"access_level":"open_access"}],"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031742330"]},"arxiv":1,"OA_type":"hybrid","oa_version":"Published Version","alternative_title":["LNCS"],"title":"Approximate distributed monitoring under partial synchrony: Balancing speed & accuracy","date_created":"2024-11-10T23:01:58Z","oa":1,"doi":"10.1007/978-3-031-74234-7_18","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).","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"month":"10","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"author":[{"first_name":"Borzoo","last_name":"Bonakdarpour","full_name":"Bonakdarpour, Borzoo"},{"full_name":"Momtaz, Anik","last_name":"Momtaz","first_name":"Anik"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"},{"last_name":"Sarac","full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","first_name":"Naci E"}],"volume":15191,"publisher":"Springer Nature","article_processing_charge":"Yes (in subscription journal)","tmp":{"short":"CC BY (4.0)","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)"},"corr_author":"1"},{"date_published":"2024-10-23T00:00:00Z","intvolume":"     15230","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2024","day":"23","citation":{"apa":"Henzinger, T. A. (2024). Reminiscences of a Real-Time Researcher. In S. Graf, P. Pettersson, &#38; B. Steffen (Eds.), <i>Real Time and Such</i> (Vol. 15230, pp. 154–164). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-73751-0_12\">https://doi.org/10.1007/978-3-031-73751-0_12</a>","mla":"Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” <i>Real Time and Such</i>, edited by Susanne Graf et al., vol. 15230, Springer Nature, 2024, pp. 154–64, doi:<a href=\"https://doi.org/10.1007/978-3-031-73751-0_12\">10.1007/978-3-031-73751-0_12</a>.","ieee":"T. A. Henzinger, “Reminiscences of a Real-Time Researcher,” in <i>Real Time and Such</i>, vol. 15230, S. Graf, P. Pettersson, and B. Steffen, Eds. Cham: Springer Nature, 2024, pp. 154–164.","short":"T.A. Henzinger, in:, S. Graf, P. Pettersson, B. Steffen (Eds.), Real Time and Such, Springer Nature, Cham, 2024, pp. 154–164.","chicago":"Henzinger, Thomas A. “Reminiscences of a Real-Time Researcher.” In <i>Real Time and Such</i>, edited by Susanne Graf, Paul Pettersson, and Bernhard Steffen, 15230:154–64. LNCS. Cham: Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-73751-0_12\">https://doi.org/10.1007/978-3-031-73751-0_12</a>.","ama":"Henzinger TA. Reminiscences of a Real-Time Researcher. In: Graf S, Pettersson P, Steffen B, eds. <i>Real Time and Such</i>. Vol 15230. LNCS. Cham: Springer Nature; 2024:154-164. doi:<a href=\"https://doi.org/10.1007/978-3-031-73751-0_12\">10.1007/978-3-031-73751-0_12</a>","ista":"Henzinger TA. 2024.Reminiscences of a Real-Time Researcher. In: Real Time and Such. LNCS, vol. 15230, 154–164."},"_id":"18563","language":[{"iso":"eng"}],"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."}],"quality_controlled":"1","type":"book_chapter","scopus_import":"1","editor":[{"last_name":"Graf","full_name":"Graf, Susanne","first_name":"Susanne"},{"last_name":"Pettersson","full_name":"Pettersson, Paul","first_name":"Paul"},{"first_name":"Bernhard","full_name":"Steffen, Bernhard","last_name":"Steffen"}],"status":"public","page":"154-164","date_updated":"2025-08-05T12:19:50Z","publication":"Real Time and Such","alternative_title":["LNCS"],"title":"Reminiscences of a Real-Time Researcher","date_created":"2024-11-18T09:10:06Z","OA_type":"closed access","oa_version":"None","place":"Cham","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031737510"],"isbn":["9783031737503"]},"publication_status":"published","series_title":"LNCS","article_processing_charge":"No","corr_author":"1","publisher":"Springer Nature","author":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"volume":15230,"department":[{"_id":"ToHe"}],"month":"10","doi":"10.1007/978-3-031-73751-0_12","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."},{"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031765537"]},"OA_type":"closed access","oa_version":"None","date_created":"2024-12-01T23:01:52Z","title":"Monitoring extended hypernode logic","alternative_title":["LNCS"],"publication_status":"published","publisher":"Springer Nature","article_processing_charge":"No","corr_author":"1","doi":"10.1007/978-3-031-76554-4_9","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, and by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502.","department":[{"_id":"ToHe"}],"month":"11","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502"}],"volume":15234,"author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","orcid":"0000-0002-8741-5799","full_name":"Oliveira da Costa, Ana","last_name":"Oliveira da Costa"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2024","intvolume":"     15234","date_published":"2024-11-13T00:00:00Z","quality_controlled":"1","type":"conference","external_id":{"isi":["001416640500009"]},"_id":"18599","language":[{"iso":"eng"}],"abstract":[{"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.","lang":"eng"}],"citation":{"apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. (2024). Monitoring extended hypernode logic. In <i>Integrated Formal Methods</i> (Vol. 15234, pp. 151–171). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">https://doi.org/10.1007/978-3-031-76554-4_9</a>","mla":"Chalupa, Marek, et al. “Monitoring Extended Hypernode Logic.” <i>Integrated Formal Methods</i>, vol. 15234, Springer Nature, 2024, pp. 151–71, doi:<a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">10.1007/978-3-031-76554-4_9</a>.","ieee":"M. Chalupa, T. A. Henzinger, and A. Oliveira da Costa, “Monitoring extended hypernode logic,” in <i>Integrated Formal Methods</i>, 2024, vol. 15234, pp. 151–171.","short":"M. Chalupa, T.A. Henzinger, A. Oliveira da Costa, in:, Integrated Formal Methods, Springer Nature, 2024, pp. 151–171.","chicago":"Chalupa, Marek, Thomas A Henzinger, and Ana Oliveira da Costa. “Monitoring Extended Hypernode Logic.” In <i>Integrated Formal Methods</i>, 15234:151–71. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">https://doi.org/10.1007/978-3-031-76554-4_9</a>.","ama":"Chalupa M, Henzinger TA, Oliveira da Costa A. Monitoring extended hypernode logic. In: <i>Integrated Formal Methods</i>. Vol 15234. Springer Nature; 2024:151-171. doi:<a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">10.1007/978-3-031-76554-4_9</a>","ista":"Chalupa M, Henzinger TA, Oliveira da Costa A. 2024. Monitoring extended hypernode logic. Integrated Formal Methods. , LNCS, vol. 15234, 151–171."},"day":"13","page":"151-171","status":"public","scopus_import":"1","ec_funded":1,"isi":1,"publication":"Integrated Formal Methods","date_updated":"2025-09-08T14:47:22Z"},{"date_updated":"2025-09-08T14:45:11Z","publication":"TOOLympics Challenge 2023","isi":1,"status":"public","page":"90-146","scopus_import":"1","external_id":{"arxiv":["2405.13583"],"isi":["001434957500004"]},"language":[{"iso":"eng"}],"_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."}],"quality_controlled":"1","type":"conference","day":"01","citation":{"mla":"Andriushchenko, Roman, et al. “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report.” <i>TOOLympics Challenge 2023</i>, vol. 14550, Springer Nature, 2024, pp. 90–146, doi:<a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">10.1007/978-3-031-67695-6_4</a>.","ieee":"R. Andriushchenko <i>et al.</i>, “Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report,” in <i>TOOLympics Challenge 2023</i>, 2024, vol. 14550, pp. 90–146.","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.","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 <i>TOOLympics Challenge 2023</i> (Vol. 14550, pp. 90–146). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">https://doi.org/10.1007/978-3-031-67695-6_4</a>","ama":"Andriushchenko R, Bork A, Budde CE, et al. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In: <i>TOOLympics Challenge 2023</i>. Vol 14550. Springer Nature; 2024:90-146. doi:<a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">10.1007/978-3-031-67695-6_4</a>","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.","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 <i>TOOLympics Challenge 2023</i>, 14550:90–146. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-67695-6_4\">https://doi.org/10.1007/978-3-031-67695-6_4</a>."},"intvolume":"     14550","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2024","OA_place":"repository","date_published":"2024-11-01T00:00:00Z","main_file_link":[{"url":" https://doi.org/10.48550/arXiv.2405.13583","open_access":"1"}],"doi":"10.1007/978-3-031-67695-6_4","oa":1,"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.","volume":14550,"author":[{"first_name":"Roman","last_name":"Andriushchenko","full_name":"Andriushchenko, Roman"},{"last_name":"Bork","full_name":"Bork, Alexander","first_name":"Alexander"},{"first_name":"Carlos E.","last_name":"Budde","full_name":"Budde, Carlos E."},{"last_name":"Češka","full_name":"Češka, Milan","first_name":"Milan"},{"last_name":"Grover","full_name":"Grover, Kush","first_name":"Kush"},{"first_name":"Ernst Moritz","full_name":"Hahn, Ernst Moritz","last_name":"Hahn"},{"first_name":"Arnd","last_name":"Hartmanns","full_name":"Hartmanns, Arnd"},{"first_name":"Bryant","full_name":"Israelsen, Bryant","last_name":"Israelsen"},{"first_name":"Nils","full_name":"Jansen, Nils","last_name":"Jansen"},{"first_name":"Joshua","last_name":"Jeppson","full_name":"Jeppson, Joshua"},{"full_name":"Junges, Sebastian","last_name":"Junges","first_name":"Sebastian"},{"full_name":"Köhl, Maximilian A.","last_name":"Köhl","first_name":"Maximilian A."},{"first_name":"Bettina","last_name":"Könighofer","full_name":"Könighofer, Bettina"},{"orcid":"0000-0002-8122-2881","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","full_name":"Kretinsky, Jan"},{"first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer"},{"last_name":"Parker","full_name":"Parker, David","first_name":"David"},{"last_name":"Pranger","full_name":"Pranger, Stefan","first_name":"Stefan"},{"first_name":"Tim","full_name":"Quatmann, Tim","last_name":"Quatmann"},{"full_name":"Ruijters, Enno","last_name":"Ruijters","first_name":"Enno"},{"last_name":"Taylor","full_name":"Taylor, Landon","first_name":"Landon"},{"first_name":"Matthias","last_name":"Volk","full_name":"Volk, Matthias"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881"},{"full_name":"Zhang, Zhen","last_name":"Zhang","first_name":"Zhen"}],"department":[{"_id":"KrCh"}],"month":"11","article_processing_charge":"No","publisher":"Springer Nature","publication_status":"published","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031676949"]},"arxiv":1,"date_created":"2024-12-01T23:01:53Z","alternative_title":["LNCS"],"title":"Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report","OA_type":"green","oa_version":"Preprint"}]