[{"month":"07","publication":"35th International Conference on Computer Aided Verification","ec_funded":1,"citation":{"apa":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In <i>35th International Conference on Computer Aided Verification</i> (Vol. 13966, pp. 3–15). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>","ama":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In: <i>35th International Conference on Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:3-15. doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>","chicago":"Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” In <i>35th International Conference on Computer Aided Verification</i>, 13966:3–15. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>.","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, in:, 35th International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 3–15.","ista":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 35th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 3–15.","mla":"Majumdar, Rupak, et al. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” <i>35th International Conference on Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 3–15, doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>.","ieee":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties,” in <i>35th International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13966, pp. 3–15."},"year":"2023","external_id":{"isi":["001310805600001"]},"has_accepted_license":"1","oa_version":"Published Version","oa":1,"file_date_updated":"2024-01-09T10:01:07Z","file":[{"content_type":"application/pdf","creator":"dernst","date_updated":"2024-01-09T10:01:07Z","file_size":405147,"checksum":"1a361d83db0244fd32c03b544c294b5a","access_level":"open_access","relation":"main_file","date_created":"2024-01-09T10:01:07Z","success":1,"file_id":"14765","file_name":"2023_LNCSCAV_Majumdar.pdf"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"volume":13966,"day":"16","article_processing_charge":"Yes (in subscription journal)","date_updated":"2025-09-09T14:16:49Z","publication_status":"published","status":"public","doi":"10.1007/978-3-031-37709-9_1","ddc":["000"],"language":[{"iso":"eng"}],"acknowledgement":"Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047.","date_created":"2024-01-08T13:18:00Z","scopus_import":"1","_id":"14758","alternative_title":["LNCS"],"intvolume":"     13966","page":"3-15","date_published":"2023-07-16T00:00:00Z","isi":1,"publisher":"Springer Nature","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"start_date":"2023-07-17","location":"Paris, France","name":"CAV: Computer Aided Verification","end_date":"2023-07-22"},"author":[{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"last_name":"Mallik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","orcid":"0000-0001-9864-7475","first_name":"Kaushik","full_name":"Mallik, Kaushik"},{"last_name":"Rychlicki","first_name":"Mateusz","full_name":"Rychlicki, Mateusz"},{"last_name":"Schmuck","first_name":"Anne-Kathrin","full_name":"Schmuck, Anne-Kathrin"},{"first_name":"Sadegh","last_name":"Soudjani","full_name":"Soudjani, Sadegh"}],"department":[{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"quality_controlled":"1","abstract":[{"text":"We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-player Rabin games. To our best knowledge, our tools are the first ones to be able to solve these problems. Furthermore, using these flexible game solvers as a back-end, we implemented a tool for computing correct-by-construction controllers for stochastic dynamical systems under LTL specifications. Our implementations use the recent theoretical result that all of these games can be solved using the same symbolic fixpoint algorithm but utilizing different, domain specific calculations of the involved predecessor operators. The main feature of our toolchain is the utilization of two programming abstractions: one to separate the symbolic fixpoint computations from the predecessor calculations, and another one to allow the integration of different BDD libraries as back-ends. In particular, we employ a multi-threaded execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan, which leads to enormous computational savings.","lang":"eng"}],"type":"conference","corr_author":"1","publication_identifier":{"isbn":["9783031377082"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031377099"]},"title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","related_material":{"record":[{"status":"public","relation":"research_data","id":"14994"}]}},{"status":"public","publication_status":"published","doi":"10.1007/978-3-031-47751-5_3","date_updated":"2025-09-09T14:22:38Z","project":[{"grant_number":"F8512","_id":"34a4ce89-11ca-11ed-8bc3-8cc37fb6e11f","name":"Security and Privacy by Design for Complex Systems"}],"volume":13951,"article_processing_charge":"No","day":"01","oa_version":"Submitted Version","oa":1,"citation":{"chicago":"Cohen, Shir, Guy Goren, Eleftherios Kokoris Kogias, Alberto Sonnino, and Alexander Spiegelman. “Proof of Availability and Retrieval in a Modular Blockchain Architecture.” In <i>27th International Conference on Financial Cryptography and Data Security</i>, 13951:36–53. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-47751-5_3\">https://doi.org/10.1007/978-3-031-47751-5_3</a>.","short":"S. Cohen, G. Goren, E. Kokoris Kogias, A. Sonnino, A. Spiegelman, in:, 27th International Conference on Financial Cryptography and Data Security, Springer Nature, 2023, pp. 36–53.","ista":"Cohen S, Goren G, Kokoris Kogias E, Sonnino A, Spiegelman A. 2023. Proof of availability and retrieval in a modular blockchain architecture. 27th International Conference on Financial Cryptography and Data Security. FC: Financial Cryptography and Data Security, LNCS, vol. 13951, 36–53.","mla":"Cohen, Shir, et al. “Proof of Availability and Retrieval in a Modular Blockchain Architecture.” <i>27th International Conference on Financial Cryptography and Data Security</i>, vol. 13951, Springer Nature, 2023, pp. 36–53, doi:<a href=\"https://doi.org/10.1007/978-3-031-47751-5_3\">10.1007/978-3-031-47751-5_3</a>.","ama":"Cohen S, Goren G, Kokoris Kogias E, Sonnino A, Spiegelman A. Proof of availability and retrieval in a modular blockchain architecture. In: <i>27th International Conference on Financial Cryptography and Data Security</i>. Vol 13951. Springer Nature; 2023:36-53. doi:<a href=\"https://doi.org/10.1007/978-3-031-47751-5_3\">10.1007/978-3-031-47751-5_3</a>","apa":"Cohen, S., Goren, G., Kokoris Kogias, E., Sonnino, A., &#38; Spiegelman, A. (2023). Proof of availability and retrieval in a modular blockchain architecture. In <i>27th International Conference on Financial Cryptography and Data Security</i> (Vol. 13951, pp. 36–53). Bol, Brac, Croatia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-47751-5_3\">https://doi.org/10.1007/978-3-031-47751-5_3</a>","ieee":"S. Cohen, G. Goren, E. Kokoris Kogias, A. Sonnino, and A. Spiegelman, “Proof of availability and retrieval in a modular blockchain architecture,” in <i>27th International Conference on Financial Cryptography and Data Security</i>, Bol, Brac, Croatia, 2023, vol. 13951, pp. 36–53."},"year":"2023","external_id":{"isi":["001150231600003"]},"month":"12","publication":"27th International Conference on Financial Cryptography and Data Security","title":"Proof of availability and retrieval in a modular blockchain architecture","type":"conference","publication_identifier":{"eisbn":["9783031477515"],"isbn":["9783031477508"],"issn":["0302-9743"],"eissn":["1611-3349"]},"main_file_link":[{"open_access":"1","url":"https://fc23.ifca.ai/preproceedings/150.pdf"}],"abstract":[{"text":"This paper explores a modular design architecture aimed at helping blockchains (and other SMR implementation) to scale to a very large number of processes. This comes in contrast to existing monolithic architectures that interleave transaction dissemination, ordering, and execution in a single functionality. To achieve this we first split the monolith to multiple layers which can use existing distributed computing primitives. The exact specifications of the data dissemination part are formally defined by the Proof of Availability & Retrieval (PoA &R) abstraction. Solutions to the PoA &R problem contain two related sub-protocols: one that “pushes” information into the network and another that “pulls” this information. Regarding the latter, there is a dearth of research literature which is rectified in this paper. We present a family of pulling sub-protocols and rigorously analyze them. Extensive simulations support the theoretical claims of efficiency and robustness in case of a very large number of players. Finally, actual implementation and deployment on a small number of machines (roughly the size of several industrial systems) demonstrates the viability of the architecture’s paradigm.","lang":"eng"}],"quality_controlled":"1","author":[{"last_name":"Cohen","first_name":"Shir","full_name":"Cohen, Shir"},{"last_name":"Goren","first_name":"Guy","full_name":"Goren, Guy"},{"id":"f5983044-d7ef-11ea-ac6d-fd1430a26d30","first_name":"Eleftherios","last_name":"Kokoris Kogias","full_name":"Kokoris Kogias, Eleftherios"},{"last_name":"Sonnino","first_name":"Alberto","full_name":"Sonnino, Alberto"},{"last_name":"Spiegelman","first_name":"Alexander","full_name":"Spiegelman, Alexander"}],"department":[{"_id":"ElKo"}],"conference":{"end_date":"2023-05-05","start_date":"2023-05-01","location":"Bol, Brac, Croatia","name":"FC: Financial Cryptography and Data Security"},"isi":1,"publisher":"Springer Nature","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","_id":"14829","intvolume":"     13951","alternative_title":["LNCS"],"page":"36-53","date_published":"2023-12-01T00:00:00Z","language":[{"iso":"eng"}],"acknowledgement":"This work is partially supported by Meta. Eleftherios Kokoris-Kogias is partially supported by Austrian Science Fund (FWF) grant No: F8512-N. Shir Cohen is supported by the Adams Fellowship Program of the Israel Academy of Sciences and Humanities.","date_created":"2024-01-18T07:41:12Z","scopus_import":"1"},{"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031327322"],"eisbn":["9783031327339"]},"corr_author":"1","type":"conference","title":"Weighted acket selection for rechargeable links in cryptocurrency networks: Complexity and approximation","related_material":{"record":[{"id":"14820","status":"public","relation":"later_version"}]},"author":[{"first_name":"Stefan","last_name":"Schmid","full_name":"Schmid, Stefan"},{"last_name":"Svoboda","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","full_name":"Svoboda, Jakub"},{"last_name":"Yeo","first_name":"Michelle X","id":"2D82B818-F248-11E8-B48F-1D18A9856A87","orcid":"0009-0001-3676-4809","full_name":"Yeo, Michelle X"}],"department":[{"_id":"KrCh"},{"_id":"KrPi"}],"abstract":[{"lang":"eng","text":"We consider a natural problem dealing with weighted packet selection across a rechargeable link, which e.g., finds applications in cryptocurrency networks. The capacity of a link (u, v) is determined by how much nodes u and v allocate for this link. Specifically, the input is a finite ordered sequence of packets that arrive in both directions along a link. Given (u, v) and a packet of weight x going from u to v, node u can either accept or reject the packet. If u accepts the packet, the capacity on link (u, v) decreases by x. Correspondingly, v’s capacity on (u, v) increases by x. If a node rejects the packet, this will entail a cost affinely linear in the weight of the packet. A link is “rechargeable” in the sense that the total capacity of the link has to remain constant, but the allocation of capacity at the ends of the link can depend arbitrarily on the nodes’ decisions. The goal is to minimise the sum of the capacity injected into the link and the cost of rejecting packets. We show that the problem is NP-hard, but can be approximated efficiently with a ratio of (1 + E) . (1 + square3) for some arbitrary E>0."}],"quality_controlled":"1","publisher":"Springer Nature","isi":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2023-06-09","name":"SIROCCO: International Colloquium on Structural Information and Communication Complexity","location":"Alcalá de Henares, Spain","start_date":"2023-06-06"},"acknowledgement":"We thank Mahsa Bastankhah and Mohammad Ali Maddah-Ali for fruitful discussions about different variants of the problem. This work is supported by the European Research Council (ERC) Consolidator Project 864228 (AdjustNet), 2020-2025, the ERC CoG 863818 (ForM-SMArt), and the German Research Foundation (DFG) grant 470029389 (FlexNets), 2021–2024.","language":[{"iso":"eng"}],"scopus_import":"1","date_created":"2025-07-10T13:15:43Z","page":"576-594","_id":"19985","intvolume":"     13892","alternative_title":["LNCS"],"date_published":"2023-05-25T00:00:00Z","date_updated":"2025-12-02T14:02:38Z","doi":"10.1007/978-3-031-32733-9_26","publication_status":"published","status":"public","oa_version":"None","OA_type":"closed access","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":"No","day":"25","volume":13892,"external_id":{"isi":["001292782600026"]},"citation":{"ieee":"S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted acket selection for rechargeable links in cryptocurrency networks: Complexity and approximation,” in <i>30th International Colloquium on Structural Information and Communication Complexity</i>, Alcalá de Henares, Spain, 2023, vol. 13892, pp. 576–594.","apa":"Schmid, S., Svoboda, J., &#38; Yeo, M. X. (2023). Weighted acket selection for rechargeable links in cryptocurrency networks: Complexity and approximation. In <i>30th International Colloquium on Structural Information and Communication Complexity</i> (Vol. 13892, pp. 576–594). Alcalá de Henares, Spain: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-32733-9_26\">https://doi.org/10.1007/978-3-031-32733-9_26</a>","ama":"Schmid S, Svoboda J, Yeo MX. Weighted acket selection for rechargeable links in cryptocurrency networks: Complexity and approximation. In: <i>30th International Colloquium on Structural Information and Communication Complexity</i>. Vol 13892. Springer Nature; 2023:576-594. doi:<a href=\"https://doi.org/10.1007/978-3-031-32733-9_26\">10.1007/978-3-031-32733-9_26</a>","chicago":"Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Acket Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” In <i>30th International Colloquium on Structural Information and Communication Complexity</i>, 13892:576–94. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-32733-9_26\">https://doi.org/10.1007/978-3-031-32733-9_26</a>.","short":"S. Schmid, J. Svoboda, M.X. Yeo, in:, 30th International Colloquium on Structural Information and Communication Complexity, Springer Nature, 2023, pp. 576–594.","mla":"Schmid, Stefan, et al. “Weighted Acket Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” <i>30th International Colloquium on Structural Information and Communication Complexity</i>, vol. 13892, Springer Nature, 2023, pp. 576–94, doi:<a href=\"https://doi.org/10.1007/978-3-031-32733-9_26\">10.1007/978-3-031-32733-9_26</a>.","ista":"Schmid S, Svoboda J, Yeo MX. 2023. Weighted acket selection for rechargeable links in cryptocurrency networks: Complexity and approximation. 30th International Colloquium on Structural Information and Communication Complexity. SIROCCO: International Colloquium on Structural Information and Communication Complexity, LNCS, vol. 13892, 576–594."},"year":"2023","publication":"30th International Colloquium on Structural Information and Communication Complexity","month":"05","ec_funded":1},{"conference":{"end_date":"2022-12-08","start_date":"2022-12-04","name":"ACCV: Asian Conference on Computer Vision","location":"Macao, China"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","extern":"1","publisher":"Springer Nature","date_published":"2023-03-11T00:00:00Z","_id":"18218","alternative_title":["LNCS"],"intvolume":"     13847","page":"518-534","date_created":"2024-10-08T12:51:14Z","scopus_import":"1","language":[{"iso":"eng"}],"related_material":{"link":[{"relation":"software","url":"https://github.com/patchadversarialattacks/patchadversarialattacks"}]},"title":"Physical passive patch adversarial attacks on visual odometry systems","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2207.05729"}],"type":"conference","arxiv":1,"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031262920"],"eisbn":["9783031262937"]},"quality_controlled":"1","abstract":[{"text":"Deep neural networks are known to be susceptible to adversarial perturbations – small perturbations that alter the output of the network and exist under strict norm limitations. While such perturbations are usually discussed as tailored to a specific input, a universal perturbation can be constructed to alter the model’s output on a set of inputs. Universal perturbations present a more realistic case of adversarial attacks, as awareness of the model’s exact input is not required. In addition, the universal attack setting raises the subject of generalization to unseen data, where given a set of inputs, the universal perturbations aim to alter the model’s output on out-of-sample data. In this work, we study physical passive patch adversarial attacks on visual odometry-based autonomous navigation systems. A visual odometry system aims to infer the relative camera motion between two corresponding viewpoints, and is frequently used by vision-based autonomous navigation systems to estimate their state. For such navigation systems, a patch adversarial perturbation poses a severe security issue, as it can be used to mislead a system onto some collision course. To the best of our knowledge, we show for the first time that the error margin of a visual odometry model can be significantly increased by deploying patch adversarial attacks in the scene. We provide evaluation on synthetic closed-loop drone navigation data and demonstrate that a comparable vulnerability exists in real data. A reference implementation of the proposed method and the reported experiments is provided at https://github.com/patchadversarialattacks/patchadversarialattacks.","lang":"eng"}],"author":[{"full_name":"Nemcovsky, Yaniv","first_name":"Yaniv","last_name":"Nemcovsky"},{"full_name":"Jacoby, Matan","first_name":"Matan","last_name":"Jacoby"},{"last_name":"Bronstein","orcid":"0000-0001-9699-8730","id":"58f3726e-7cba-11ef-ad8b-e6e8cb3904e6","first_name":"Alexander","full_name":"Bronstein, Alexander"},{"last_name":"Baskin","first_name":"Chaim","full_name":"Baskin, Chaim"}],"year":"2023","citation":{"chicago":"Nemcovsky, Yaniv, Matan Jacoby, Alex M. Bronstein, and Chaim Baskin. “Physical Passive Patch Adversarial Attacks on Visual Odometry Systems.” In <i>16th Asian Conference on Computer Vision</i>, 13847:518–34. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-26293-7_31\">https://doi.org/10.1007/978-3-031-26293-7_31</a>.","mla":"Nemcovsky, Yaniv, et al. “Physical Passive Patch Adversarial Attacks on Visual Odometry Systems.” <i>16th Asian Conference on Computer Vision</i>, vol. 13847, Springer Nature, 2023, pp. 518–34, doi:<a href=\"https://doi.org/10.1007/978-3-031-26293-7_31\">10.1007/978-3-031-26293-7_31</a>.","short":"Y. Nemcovsky, M. Jacoby, A.M. Bronstein, C. Baskin, in:, 16th Asian Conference on Computer Vision, Springer Nature, 2023, pp. 518–534.","ista":"Nemcovsky Y, Jacoby M, Bronstein AM, Baskin C. 2023. Physical passive patch adversarial attacks on visual odometry systems. 16th Asian Conference on Computer Vision. ACCV: Asian Conference on Computer Vision, LNCS, vol. 13847, 518–534.","ama":"Nemcovsky Y, Jacoby M, Bronstein AM, Baskin C. Physical passive patch adversarial attacks on visual odometry systems. In: <i>16th Asian Conference on Computer Vision</i>. Vol 13847. Springer Nature; 2023:518-534. doi:<a href=\"https://doi.org/10.1007/978-3-031-26293-7_31\">10.1007/978-3-031-26293-7_31</a>","apa":"Nemcovsky, Y., Jacoby, M., Bronstein, A. M., &#38; Baskin, C. (2023). Physical passive patch adversarial attacks on visual odometry systems. In <i>16th Asian Conference on Computer Vision</i> (Vol. 13847, pp. 518–534). Macao, China: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-26293-7_31\">https://doi.org/10.1007/978-3-031-26293-7_31</a>","ieee":"Y. Nemcovsky, M. Jacoby, A. M. Bronstein, and C. Baskin, “Physical passive patch adversarial attacks on visual odometry systems,” in <i>16th Asian Conference on Computer Vision</i>, Macao, China, 2023, vol. 13847, pp. 518–534."},"external_id":{"arxiv":["2207.05729"]},"month":"03","publication":"16th Asian Conference on Computer Vision","status":"public","publication_status":"published","doi":"10.1007/978-3-031-26293-7_31","date_updated":"2024-10-09T12:13:36Z","volume":13847,"day":"11","article_processing_charge":"No","oa":1,"oa_version":"Preprint"},{"date_created":"2022-03-20T23:01:40Z","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"The formal framework for quantitative monitoring which is presented in this invited talk was defined jointly with N. Ege Saraç at LICS 2021. This work was supported in part by the Wittgenstein Award Z211-N23 of the Austrian Science Fund.","date_published":"2022-02-22T00:00:00Z","_id":"10891","intvolume":"     13124","page":"3-6","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","isi":1,"publisher":"Springer Nature","conference":{"end_date":"2021-10-19","name":"NSV: Numerical Software Verification","location":"New Haven, CT, United States","start_date":"2021-10-18"},"department":[{"_id":"ToHe"}],"author":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724"}],"quality_controlled":"1","abstract":[{"text":"We present a formal framework for the online black-box monitoring of software using monitors with quantitative verdict functions. Quantitative verdict functions have several advantages. First, quantitative monitors can be approximate, i.e., the value of the verdict function does not need to correspond exactly to the value of the property under observation. Second, quantitative monitors can be quantified universally, i.e., for every possible observed behavior, the monitor tries to make the best effort to estimate the value of the property under observation. Third, quantitative monitors can watch boolean as well as quantitative properties, such as average response time. Fourth, quantitative monitors can use non-finite-state resources, such as counters. As a consequence, quantitative monitors can be compared according to how many resources they use (e.g., the number of counters) and how precisely they approximate the property under observation. This allows for a rich spectrum of cost-precision trade-offs in monitoring software.","lang":"eng"}],"corr_author":"1","type":"conference","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783030955601"]},"series_title":"LNCS","title":"Quantitative monitoring of software","month":"02","publication":"Software Verification","citation":{"ieee":"T. A. Henzinger, “Quantitative monitoring of software,” in <i>Software Verification</i>, New Haven, CT, United States, 2022, vol. 13124, pp. 3–6.","mla":"Henzinger, Thomas A. “Quantitative Monitoring of Software.” <i>Software Verification</i>, vol. 13124, Springer Nature, 2022, pp. 3–6, doi:<a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">10.1007/978-3-030-95561-8_1</a>.","ista":"Henzinger TA. 2022. Quantitative monitoring of software. Software Verification. NSV: Numerical Software VerificationLNCS vol. 13124, 3–6.","short":"T.A. Henzinger, in:, Software Verification, Springer Nature, 2022, pp. 3–6.","chicago":"Henzinger, Thomas A. “Quantitative Monitoring of Software.” In <i>Software Verification</i>, 13124:3–6. LNCS. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">https://doi.org/10.1007/978-3-030-95561-8_1</a>.","ama":"Henzinger TA. Quantitative monitoring of software. In: <i>Software Verification</i>. Vol 13124. LNCS. Springer Nature; 2022:3-6. doi:<a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">10.1007/978-3-030-95561-8_1</a>","apa":"Henzinger, T. A. (2022). Quantitative monitoring of software. In <i>Software Verification</i> (Vol. 13124, pp. 3–6). New Haven, CT, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-95561-8_1\">https://doi.org/10.1007/978-3-030-95561-8_1</a>"},"year":"2022","external_id":{"isi":["000771713200001"]},"oa_version":"None","volume":13124,"article_processing_charge":"No","day":"22","project":[{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"date_updated":"2025-04-15T06:25:58Z","publication_status":"published","status":"public","doi":"10.1007/978-3-030-95561-8_1"},{"year":"2022","citation":{"ieee":"A. M. Arroyo Guevara and S. Felsner, “Approximating the bundled crossing number,” in <i>WALCOM 2022: Algorithms and Computation</i>, Jember, Indonesia, 2022, vol. 13174, pp. 383–395.","mla":"Arroyo Guevara, Alan M., and Stefan Felsner. “Approximating the Bundled Crossing Number.” <i>WALCOM 2022: Algorithms and Computation</i>, vol. 13174, Springer Nature, 2022, pp. 383–95, doi:<a href=\"https://doi.org/10.1007/978-3-030-96731-4_31\">10.1007/978-3-030-96731-4_31</a>.","ista":"Arroyo Guevara AM, Felsner S. 2022. Approximating the bundled crossing number. WALCOM 2022: Algorithms and Computation. WALCOM: Algorithms and ComputationLNCS vol. 13174, 383–395.","short":"A.M. Arroyo Guevara, S. Felsner, in:, WALCOM 2022: Algorithms and Computation, Springer Nature, 2022, pp. 383–395.","chicago":"Arroyo Guevara, Alan M, and Stefan Felsner. “Approximating the Bundled Crossing Number.” In <i>WALCOM 2022: Algorithms and Computation</i>, 13174:383–95. LNCS. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-96731-4_31\">https://doi.org/10.1007/978-3-030-96731-4_31</a>.","apa":"Arroyo Guevara, A. M., &#38; Felsner, S. (2022). Approximating the bundled crossing number. In <i>WALCOM 2022: Algorithms and Computation</i> (Vol. 13174, pp. 383–395). Jember, Indonesia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-96731-4_31\">https://doi.org/10.1007/978-3-030-96731-4_31</a>","ama":"Arroyo Guevara AM, Felsner S. Approximating the bundled crossing number. In: <i>WALCOM 2022: Algorithms and Computation</i>. Vol 13174. LNCS. Springer Nature; 2022:383-395. doi:<a href=\"https://doi.org/10.1007/978-3-030-96731-4_31\">10.1007/978-3-030-96731-4_31</a>"},"external_id":{"arxiv":["2109.14892"],"isi":["001435074700031"]},"ec_funded":1,"publication":"WALCOM 2022: Algorithms and Computation","month":"03","publication_status":"published","status":"public","doi":"10.1007/978-3-030-96731-4_31","date_updated":"2025-09-10T09:35:56Z","project":[{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"}],"volume":13174,"day":"16","article_processing_charge":"No","oa_version":"Preprint","oa":1,"conference":{"name":"WALCOM: Algorithms and Computation","location":"Jember, Indonesia","start_date":"2022-03-24","end_date":"2022-03-26"},"isi":1,"publisher":"Springer Nature","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","intvolume":"     13174","_id":"11185","page":"383-395","date_published":"2022-03-16T00:00:00Z","language":[{"iso":"eng"}],"acknowledgement":"This work was initiated during the Workshop on Geometric Graphs in November 2019 in Strobl, Austria. We would like to thank Oswin Aichholzer, Fabian Klute, Man-Kwun Chiu, Martin Balko, Pavel Valtr for their avid discussions during the workshop. The first author has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska Curie grant agreement No 754411. The second author has been supported by the German Research Foundation DFG Project FE 340/12-1.","date_created":"2022-04-17T22:01:47Z","scopus_import":"1","title":"Approximating the bundled crossing number","related_material":{"record":[{"id":"13969","status":"public","relation":"later_version"}]},"series_title":"LNCS","type":"conference","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783030967307"]},"arxiv":1,"main_file_link":[{"url":" https://doi.org/10.48550/arXiv.2109.14892","open_access":"1"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"Bundling crossings is a strategy which can enhance the readability of graph drawings. In this paper we consider bundlings for families of pseudosegments, i.e., simple curves such that any two have share at most one point at which they cross. Our main result is that there is a polynomial-time algorithm to compute an 8-approximation of the bundled crossing number of such instances (up to adding a term depending on the facial structure). This 8-approximation also holds for bundlings of good drawings of graphs. In the special case of circular drawings the approximation factor is 8 (no extra term), this improves upon the 10-approximation of Fink et al. [6]. We also show how to compute a 92-approximation when the intersection graph of the pseudosegments is bipartite."}],"author":[{"full_name":"Arroyo Guevara, Alan M","id":"3207FDC6-F248-11E8-B48F-1D18A9856A87","first_name":"Alan M","orcid":"0000-0003-2401-8670","last_name":"Arroyo Guevara"},{"full_name":"Felsner, Stefan","last_name":"Felsner","first_name":"Stefan"}],"department":[{"_id":"UlWa"}]},{"doi":"10.1007/978-3-030-99429-7_1","status":"public","publication_status":"published","ddc":["000"],"date_updated":"2025-12-30T06:50:51Z","file_date_updated":"2022-05-09T06:52:44Z","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"file":[{"content_type":"application/pdf","file_size":479146,"date_updated":"2022-05-09T06:52:44Z","creator":"dernst","relation":"main_file","access_level":"open_access","checksum":"7f6f860b20b8de2a249e9c1b4eee15cf","file_name":"2022_LNCS_Bartocci.pdf","file_id":"11357","success":1,"date_created":"2022-05-09T06:52:44Z"}],"article_processing_charge":"No","day":"29","volume":13241,"oa_version":"Published Version","oa":1,"has_accepted_license":"1","external_id":{"isi":["000782393600001"]},"citation":{"ieee":"E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa, “Information-flow interfaces,” in <i>Fundamental Approaches to Software Engineering</i>, Munich, Germany, 2022, vol. 13241, pp. 3–22.","ama":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Information-flow interfaces. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13241. Springer Nature; 2022:3-22. doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>","apa":"Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Da Costa, A. O. (2022). Information-flow interfaces. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13241, pp. 3–22). Munich, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>","chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira Da Costa. “Information-Flow Interfaces.” In <i>Fundamental Approaches to Software Engineering</i>, 13241:3–22. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">https://doi.org/10.1007/978-3-030-99429-7_1</a>.","ista":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Information-flow interfaces. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13241, 3–22.","short":"E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2022, pp. 3–22.","mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13241, Springer Nature, 2022, pp. 3–22, doi:<a href=\"https://doi.org/10.1007/978-3-030-99429-7_1\">10.1007/978-3-030-99429-7_1</a>."},"year":"2022","ec_funded":1,"publication":"Fundamental Approaches to Software Engineering","month":"03","title":"Information-flow interfaces","related_material":{"record":[{"status":"public","relation":"extended_version","id":"17094"}]},"publication_identifier":{"isbn":["9783030994280"],"eissn":["1611-3349"],"issn":["0302-9743"]},"type":"conference","abstract":[{"lang":"eng","text":"Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees.\r\nAlthough there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory that is designed for ensuring system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. We illustrate the applicability of our framework with an example inspired from the automotive domain."}],"quality_controlled":"1","author":[{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","first_name":"Thomas","last_name":"Ferrere"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"last_name":"Nickovic","first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"},{"last_name":"Da Costa","first_name":"Ana Oliveira","full_name":"Da Costa, Ana Oliveira"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"ToHe"}],"conference":{"end_date":"2022-04-07","name":"FASE: Fundamental Approaches to Software Engineering","location":"Munich, Germany","start_date":"2022-04-02"},"publisher":"Springer Nature","isi":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","page":"3-22","_id":"11355","alternative_title":["LNCS"],"intvolume":"     13241","date_published":"2022-03-29T00:00:00Z","acknowledgement":"This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 956123 and was funded in part by the FWF project W1255-N23 and by the ERC-2020-AdG 101020093.","language":[{"iso":"eng"}],"scopus_import":"1","date_created":"2022-05-08T22:01:44Z"},{"publisher":"Springer Nature","citation":{"ieee":"F. Karimipour and S. Storandt, Eds., <i>Web and Wireless Geographical Information Systems</i>, 1st ed., vol. 13238. Cham: Springer Nature, 2022.","ama":"Karimipour F, Storandt S, eds. <i>Web and Wireless Geographical Information Systems</i>. Vol 13238. 1st ed. Cham: Springer Nature; 2022. doi:<a href=\"https://doi.org/10.1007/978-3-031-06245-2\">10.1007/978-3-031-06245-2</a>","apa":"Karimipour, F., &#38; Storandt, S. (Eds.). (2022). <i>Web and Wireless Geographical Information Systems</i> (1st ed., Vol. 13238). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-06245-2\">https://doi.org/10.1007/978-3-031-06245-2</a>","mla":"Karimipour, Farid, and Sabine Storandt, editors. <i>Web and Wireless Geographical Information Systems</i>. 1st ed., vol. 13238, Springer Nature, 2022, doi:<a href=\"https://doi.org/10.1007/978-3-031-06245-2\">10.1007/978-3-031-06245-2</a>.","ista":"Karimipour F, Storandt S eds. 2022. Web and Wireless Geographical Information Systems 1st ed., Cham: Springer Nature, 153p.","short":"F. Karimipour, S. Storandt, eds., Web and Wireless Geographical Information Systems, 1st ed., Springer Nature, Cham, 2022.","chicago":"Karimipour, Farid, and Sabine Storandt, eds. <i>Web and Wireless Geographical Information Systems</i>. 1st ed. Vol. 13238. Cham: Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-06245-2\">https://doi.org/10.1007/978-3-031-06245-2</a>."},"year":"2022","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","edition":"1","place":"Cham","page":"153","intvolume":"     13238","_id":"11429","alternative_title":["LNCS"],"date_published":"2022-05-01T00:00:00Z","month":"05","language":[{"iso":"eng"}],"date_created":"2022-06-02T05:40:53Z","title":"Web and Wireless Geographical Information Systems","doi":"10.1007/978-3-031-06245-2","status":"public","publication_status":"published","publication_identifier":{"isbn":["9783031062445"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031062452"]},"corr_author":"1","editor":[{"orcid":"0000-0001-6746-4174","id":"2A2BCDC4-CF62-11E9-BE5E-3B1EE6697425","first_name":"Farid","last_name":"Karimipour","full_name":"Karimipour, Farid"},{"full_name":"Storandt, Sabine","last_name":"Storandt","first_name":"Sabine"}],"type":"book_editor","date_updated":"2024-10-09T21:02:30Z","quality_controlled":"1","day":"01","article_processing_charge":"No","abstract":[{"lang":"eng","text":"This book constitutes the refereed proceedings of the 18th International Symposium on Web and Wireless Geographical Information Systems, W2GIS 2022, held in Konstanz, Germany, in April 2022.\r\nThe 7 full papers presented together with 6 short papers in the volume were carefully reviewed and selected from 16 submissions.  The papers cover topics that range from mobile GIS and Location-Based Services to Spatial Information Retrieval and Wireless Sensor Networks."}],"volume":13238,"oa_version":"None","department":[{"_id":"HeEd"}]},{"date_published":"2022-05-25T00:00:00Z","_id":"11476","intvolume":"     13276","alternative_title":["LNCS"],"page":"815–844","date_created":"2022-06-30T16:48:00Z","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"We thank Marta Mularczyk and Yiannis Tselekounis for their very helpful feedback on an earlier draft of this paper.","conference":{"location":"Trondheim, Norway","name":"EUROCRYPT: Theory and Applications of Cryptology and Information Security","start_date":"2022-05-30","end_date":"2022-06-03"},"place":"Cham","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","isi":1,"publisher":"Springer Nature","abstract":[{"text":"Messaging platforms like Signal are widely deployed and provide strong security in an asynchronous setting. It is a challenging problem to construct a protocol with similar security guarantees that can efficiently scale to large groups. A major bottleneck are the frequent key rotations users need to perform to achieve post compromise forward security.\r\n\r\nIn current proposals – most notably in TreeKEM (which is part of the IETF’s Messaging Layer Security (MLS) protocol draft) – for users in a group of size n to rotate their keys, they must each craft a message of size log(n) to be broadcast to the group using an (untrusted) delivery server.\r\n\r\nIn larger groups, having users sequentially rotate their keys requires too much bandwidth (or takes too long), so variants allowing any T≤n users to simultaneously rotate their keys in just 2 communication rounds have been suggested (e.g. “Propose and Commit” by MLS). Unfortunately, 2-round concurrent updates are either damaging or expensive (or both); i.e. they either result in future operations being more costly (e.g. via “blanking” or “tainting”) or are costly themselves requiring Ω(T) communication for each user [Bienstock et al., TCC’20].\r\n\r\nIn this paper we propose CoCoA; a new scheme that allows for T concurrent updates that are neither damaging nor costly. That is, they add no cost to future operations yet they only require Ω(log2(n)) communication per user. To circumvent the [Bienstock et al.] lower bound, CoCoA increases the number of rounds needed to complete all updates from 2 up to (at most) log(n); though typically fewer rounds are needed.\r\n\r\nThe key insight of our protocol is the following: in the (non-concurrent version of) TreeKEM, a delivery server which gets T concurrent update requests will approve one and reject the remaining T−1. In contrast, our server attempts to apply all of them. If more than one user requests to rotate the same key during a round, the server arbitrarily picks a winner. Surprisingly, we prove that regardless of how the server chooses the winners, all previously compromised users will recover after at most log(n) such update rounds.\r\n\r\nTo keep the communication complexity low, CoCoA is a server-aided CGKA. That is, the delivery server no longer blindly forwards packets, but instead actively computes individualized packets tailored to each user. As the server is untrusted, this change requires us to develop new mechanisms ensuring robustness of the protocol.","lang":"eng"}],"quality_controlled":"1","department":[{"_id":"GradSch"},{"_id":"KrPi"}],"author":[{"full_name":"Alwen, Joël","last_name":"Alwen","first_name":"Joël"},{"id":"D33D2B18-E445-11E9-ABB7-15F4E5697425","first_name":"Benedikt","orcid":"0000-0002-7553-6606","last_name":"Auerbach","full_name":"Auerbach, Benedikt"},{"last_name":"Cueto Noval","id":"ffc563a3-f6e0-11ea-865d-e3cce03d17cc","first_name":"Miguel","orcid":"0000-0002-2505-4246","full_name":"Cueto Noval, Miguel"},{"full_name":"Klein, Karen","id":"3E83A2F8-F248-11E8-B48F-1D18A9856A87","first_name":"Karen","last_name":"Klein"},{"full_name":"Pascual Perez, Guillermo","last_name":"Pascual Perez","first_name":"Guillermo","orcid":"0000-0001-8630-415X","id":"2D7ABD02-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pietrzak, Krzysztof Z","last_name":"Pietrzak","orcid":"0000-0002-9139-1654","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","first_name":"Krzysztof Z"},{"last_name":"Walter","first_name":"Michael","full_name":"Walter, Michael"}],"related_material":{"record":[{"id":"18088","status":"public","relation":"dissertation_contains"}]},"title":"CoCoA: Concurrent continuous group key agreement","main_file_link":[{"url":"https://eprint.iacr.org/2022/251","open_access":"1"}],"type":"conference","corr_author":"1","publication_identifier":{"eisbn":["9783031070853"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031070846"]},"ec_funded":1,"publication":"Advances in Cryptology – EUROCRYPT 2022","month":"05","year":"2022","citation":{"ieee":"J. Alwen <i>et al.</i>, “CoCoA: Concurrent continuous group key agreement,” in <i>Advances in Cryptology – EUROCRYPT 2022</i>, Trondheim, Norway, 2022, vol. 13276, pp. 815–844.","mla":"Alwen, Joël, et al. “CoCoA: Concurrent Continuous Group Key Agreement.” <i>Advances in Cryptology – EUROCRYPT 2022</i>, vol. 13276, Springer Nature, 2022, pp. 815–844, doi:<a href=\"https://doi.org/10.1007/978-3-031-07085-3_28\">10.1007/978-3-031-07085-3_28</a>.","short":"J. Alwen, B. Auerbach, M. Cueto Noval, K. Klein, G. Pascual Perez, K.Z. Pietrzak, M. Walter, in:, Advances in Cryptology – EUROCRYPT 2022, Springer Nature, Cham, 2022, pp. 815–844.","ista":"Alwen J, Auerbach B, Cueto Noval M, Klein K, Pascual Perez G, Pietrzak KZ, Walter M. 2022. CoCoA: Concurrent continuous group key agreement. Advances in Cryptology – EUROCRYPT 2022. EUROCRYPT: Theory and Applications of Cryptology and Information Security, LNCS, vol. 13276, 815–844.","chicago":"Alwen, Joël, Benedikt Auerbach, Miguel Cueto Noval, Karen Klein, Guillermo Pascual Perez, Krzysztof Z Pietrzak, and Michael Walter. “CoCoA: Concurrent Continuous Group Key Agreement.” In <i>Advances in Cryptology – EUROCRYPT 2022</i>, 13276:815–844. Cham: Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-07085-3_28\">https://doi.org/10.1007/978-3-031-07085-3_28</a>.","apa":"Alwen, J., Auerbach, B., Cueto Noval, M., Klein, K., Pascual Perez, G., Pietrzak, K. Z., &#38; Walter, M. (2022). CoCoA: Concurrent continuous group key agreement. In <i>Advances in Cryptology – EUROCRYPT 2022</i> (Vol. 13276, pp. 815–844). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-07085-3_28\">https://doi.org/10.1007/978-3-031-07085-3_28</a>","ama":"Alwen J, Auerbach B, Cueto Noval M, et al. CoCoA: Concurrent continuous group key agreement. In: <i>Advances in Cryptology – EUROCRYPT 2022</i>. Vol 13276. Cham: Springer Nature; 2022:815–844. doi:<a href=\"https://doi.org/10.1007/978-3-031-07085-3_28\">10.1007/978-3-031-07085-3_28</a>"},"external_id":{"isi":["000832305300028"]},"volume":13276,"article_processing_charge":"No","day":"25","project":[{"grant_number":"682815","name":"Teaching Old Crypto New Tricks","_id":"258AA5B2-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"oa":1,"oa_version":"Preprint","publication_status":"published","status":"public","doi":"10.1007/978-3-031-07085-3_28","date_updated":"2026-04-07T13:01:26Z"},{"acknowledgement":"This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 840605. This work was supported in part by the Academy of Finland, Grants 314888 and 333837. The authors would also like to thank David Harris, Neven Villani, and the anonymous reviewers for their very helpful comments and feedback on previous versions of this work.","language":[{"iso":"eng"}],"scopus_import":"1","date_created":"2022-07-31T22:01:49Z","page":"1-20","intvolume":"     13298","_id":"11707","date_published":"2022-06-25T00:00:00Z","publisher":"Springer Nature","isi":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","conference":{"start_date":"2022-06-27","name":"SIROCCO: Structural Information and Communication Complexity","location":"Paderborn, Germany","end_date":"2022-06-29"},"author":[{"first_name":"Alkida","last_name":"Balliu","full_name":"Balliu, Alkida"},{"full_name":"Hirvonen, Juho","last_name":"Hirvonen","first_name":"Juho"},{"last_name":"Melnyk","first_name":"Darya","full_name":"Melnyk, Darya"},{"last_name":"Olivetti","first_name":"Dennis","full_name":"Olivetti, Dennis"},{"last_name":"Rybicki","orcid":"0000-0002-6432-6646","first_name":"Joel","id":"334EFD2E-F248-11E8-B48F-1D18A9856A87","full_name":"Rybicki, Joel"},{"full_name":"Suomela, Jukka","first_name":"Jukka","last_name":"Suomela"}],"department":[{"_id":"DaAl"}],"abstract":[{"lang":"eng","text":"In this work we introduce the graph-theoretic notion of mendability: for each locally checkable graph problem we can define its mending radius, which captures the idea of how far one needs to modify a partial solution in order to “patch a hole.” We explore how mendability is connected to the existence of efficient algorithms, especially in distributed, parallel, and fault-tolerant settings. It is easy to see that O(1)-mendable problems are also solvable in O(log∗n) rounds in the LOCAL model of distributed computing. One of the surprises is that in paths and cycles, a converse also holds in the following sense: if a problem Π can be solved in O(log∗n), there is always a restriction Π′⊆Π that is still efficiently solvable but that is also O(1)-mendable. We also explore the structure of the landscape of mendability. For example, we show that in trees, the mending radius of any locally checkable problem is O(1), Θ(logn), or Θ(n), while in general graphs the structure is much more diverse."}],"quality_controlled":"1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031099922"]},"arxiv":1,"type":"conference","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2102.08703"}],"title":"Local mending","series_title":"LNCS","month":"06","publication":"International Colloquium on Structural Information and Communication Complexity","ec_funded":1,"external_id":{"isi":["000876977400001"],"arxiv":["2102.08703"]},"year":"2022","citation":{"apa":"Balliu, A., Hirvonen, J., Melnyk, D., Olivetti, D., Rybicki, J., &#38; Suomela, J. (2022). Local mending. In M. Parter (Ed.), <i>International Colloquium on Structural Information and Communication Complexity</i> (Vol. 13298, pp. 1–20). Paderborn, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-09993-9_1\">https://doi.org/10.1007/978-3-031-09993-9_1</a>","ama":"Balliu A, Hirvonen J, Melnyk D, Olivetti D, Rybicki J, Suomela J. Local mending. In: Parter M, ed. <i>International Colloquium on Structural Information and Communication Complexity</i>. Vol 13298. LNCS. Springer Nature; 2022:1-20. doi:<a href=\"https://doi.org/10.1007/978-3-031-09993-9_1\">10.1007/978-3-031-09993-9_1</a>","chicago":"Balliu, Alkida, Juho Hirvonen, Darya Melnyk, Dennis Olivetti, Joel Rybicki, and Jukka Suomela. “Local Mending.” In <i>International Colloquium on Structural Information and Communication Complexity</i>, edited by Merav Parter, 13298:1–20. LNCS. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-09993-9_1\">https://doi.org/10.1007/978-3-031-09993-9_1</a>.","mla":"Balliu, Alkida, et al. “Local Mending.” <i>International Colloquium on Structural Information and Communication Complexity</i>, edited by Merav Parter, vol. 13298, Springer Nature, 2022, pp. 1–20, doi:<a href=\"https://doi.org/10.1007/978-3-031-09993-9_1\">10.1007/978-3-031-09993-9_1</a>.","short":"A. Balliu, J. Hirvonen, D. Melnyk, D. Olivetti, J. Rybicki, J. Suomela, in:, M. Parter (Ed.), International Colloquium on Structural Information and Communication Complexity, Springer Nature, 2022, pp. 1–20.","ista":"Balliu A, Hirvonen J, Melnyk D, Olivetti D, Rybicki J, Suomela J. 2022. Local mending. International Colloquium on Structural Information and Communication Complexity. SIROCCO: Structural Information and Communication ComplexityLNCS vol. 13298, 1–20.","ieee":"A. Balliu, J. Hirvonen, D. Melnyk, D. Olivetti, J. Rybicki, and J. Suomela, “Local mending,” in <i>International Colloquium on Structural Information and Communication Complexity</i>, Paderborn, Germany, 2022, vol. 13298, pp. 1–20."},"oa_version":"Preprint","oa":1,"project":[{"call_identifier":"H2020","_id":"26A5D39A-B435-11E9-9278-68D0E5697425","name":"Coordination in constrained and natural distributed systems","grant_number":"840605"}],"article_processing_charge":"No","day":"25","volume":13298,"editor":[{"last_name":"Parter","first_name":"Merav","full_name":"Parter, Merav"}],"date_updated":"2025-04-14T07:50:55Z","doi":"10.1007/978-3-031-09993-9_1","status":"public","publication_status":"published"},{"intvolume":"     13498","_id":"11775","alternative_title":["LNCS"],"page":"200-220","date_published":"2022-09-23T00:00:00Z","language":[{"iso":"eng"}],"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","date_created":"2022-08-08T17:09:09Z","scopus_import":"1","conference":{"end_date":"2022-09-30","start_date":"2022-09-28","location":"Tbilisi, Georgia","name":"RV: Runtime Verification"},"isi":1,"publisher":"Springer Nature","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","abstract":[{"lang":"eng","text":"Quantitative monitoring can be universal and approximate: For every finite sequence of observations, the specification provides a value and the monitor outputs a best-effort approximation of it. The quality of the approximation may depend on the resources that are available to the monitor. By taking to the limit the sequences of specification values and monitor outputs, we obtain precision-resource trade-offs also for limit monitoring. This paper provides a formal framework for studying such trade-offs using an abstract interpretation for monitors: For each natural number n, the aggregate semantics of a monitor at time n is an equivalence relation over all sequences of at most n observations so that two equivalent sequences are indistinguishable to the monitor and thus mapped to the same output. This abstract interpretation of quantitative monitors allows us to measure the number of equivalence classes (or “resource use”) that is necessary for a certain precision up to a certain time, or at any time. Our framework offers several insights. For example, we identify a family of specifications for which any resource-optimal exact limit monitor is independent of any error permitted over finite traces. Moreover, we present a specification for which any resource-optimal approximate limit monitor does not minimize its resource use at any time. "}],"quality_controlled":"1","author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"},{"last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E"}],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"title":"Abstract monitors for quantitative specifications","related_material":{"record":[{"id":"20147","relation":"dissertation_contains","status":"public"}]},"corr_author":"1","type":"conference","publication_identifier":{"issn":["0302-9743"]},"ec_funded":1,"publication":"22nd International Conference on Runtime Verification","month":"09","has_accepted_license":"1","year":"2022","citation":{"ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Abstract monitors for quantitative specifications. In: <i>22nd International Conference on Runtime Verification</i>. Vol 13498. Springer Nature; 2022:200-220. doi:<a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">10.1007/978-3-031-17196-3_11</a>","apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2022). Abstract monitors for quantitative specifications. In <i>22nd International Conference on Runtime Verification</i> (Vol. 13498, pp. 200–220). Tbilisi, Georgia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">https://doi.org/10.1007/978-3-031-17196-3_11</a>","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Abstract Monitors for Quantitative Specifications.” In <i>22nd International Conference on Runtime Verification</i>, 13498:200–220. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">https://doi.org/10.1007/978-3-031-17196-3_11</a>.","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2022. Abstract monitors for quantitative specifications. 22nd International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 13498, 200–220.","mla":"Henzinger, Thomas A., et al. “Abstract Monitors for Quantitative Specifications.” <i>22nd International Conference on Runtime Verification</i>, vol. 13498, Springer Nature, 2022, pp. 200–20, doi:<a href=\"https://doi.org/10.1007/978-3-031-17196-3_11\">10.1007/978-3-031-17196-3_11</a>.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 22nd International Conference on Runtime Verification, Springer Nature, 2022, pp. 200–220.","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Abstract monitors for quantitative specifications,” in <i>22nd International Conference on Runtime Verification</i>, Tbilisi, Georgia, 2022, vol. 13498, pp. 200–220."},"external_id":{"isi":["000866539700011"]},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"file":[{"success":1,"file_id":"12317","file_name":"2022_LNCS_RV_Henzinger.pdf","date_created":"2023-01-20T07:34:50Z","relation":"main_file","checksum":"05c7dcfbb9053a98f46441fb2eccb213","access_level":"open_access","date_updated":"2023-01-20T07:34:50Z","file_size":477110,"creator":"dernst","content_type":"application/pdf"}],"file_date_updated":"2023-01-20T07:34:50Z","volume":13498,"day":"23","article_processing_charge":"Yes","oa_version":"Published Version","oa":1,"status":"public","publication_status":"published","doi":"10.1007/978-3-031-17196-3_11","ddc":["000"],"date_updated":"2026-04-07T12:02:56Z"},{"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031131844"]},"type":"conference","title":"Sound and complete certificates for auantitative termination analysis of probabilistic programs","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"14539"}]},"author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","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"},{"last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","first_name":"Tobias","full_name":"Meggendorfer, Tobias"},{"last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","full_name":"Zikelic, Dorde"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"KrCh"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold p∈[0,1], we aim for certificates proving that the program terminates with probability at least 1−p. The basic idea of our approach is to find a terminating stochastic invariant, i.e. a subset SI of program states such that (i) the probability of the program ever leaving SI is no more than p, and (ii) almost-surely, the program either leaves SI or terminates.\r\n\r\nWhile stochastic invariants are already well-known, we provide the first proof that the idea above is not only sound, but also complete for quantitative termination analysis. We then introduce a novel sound and complete characterization of stochastic invariants that enables template-based approaches for easy synthesis of quantitative termination certificates, especially in affine or polynomial forms. Finally, by combining this idea with the existing martingale-based methods that are relatively complete for qualitative termination analysis, we obtain the first automated, sound, and relatively complete algorithm for quantitative termination analysis. Notably, our completeness guarantees for quantitative termination analysis are as strong as the best-known methods for the qualitative variant.\r\n\r\nOur prototype implementation demonstrates the effectiveness of our approach on various probabilistic programs. We also demonstrate that our algorithm certifies lower bounds on termination probability for probabilistic programs that are beyond the reach of previous methods."}],"publisher":"Springer","isi":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","conference":{"start_date":"2022-08-07","name":"CAV: Computer Aided Verification","location":"Haifa, Israel","end_date":"2022-08-10"},"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the HKUST-Kaisa Joint Research Institute Project Grant HKJRI3A-055, the HKUST Startup Grant R9272 and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","language":[{"iso":"eng"}],"scopus_import":"1","date_created":"2022-08-28T22:02:02Z","page":"55-78","intvolume":"     13371","_id":"12000","alternative_title":["LNCS"],"date_published":"2022-08-07T00:00:00Z","date_updated":"2026-04-07T13:27:55Z","doi":"10.1007/978-3-031-13185-1_4","status":"public","publication_status":"published","ddc":["000"],"oa_version":"Published Version","oa":1,"file_date_updated":"2022-08-29T09:17:01Z","file":[{"success":1,"file_name":"2022_LNCS_Chatterjee.pdf","file_id":"12003","date_created":"2022-08-29T09:17:01Z","relation":"main_file","access_level":"open_access","checksum":"24e0f810ec52735a90ade95198bc641d","date_updated":"2022-08-29T09:17:01Z","file_size":505094,"creator":"alisjak","content_type":"application/pdf"}],"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"}],"article_processing_charge":"Yes (in subscription journal)","day":"07","volume":13371,"external_id":{"isi":["000870304500004"]},"citation":{"ieee":"K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic, “Sound and complete certificates for auantitative termination analysis of probabilistic programs,” in <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>, Haifa, Israel, 2022, vol. 13371, pp. 55–78.","ama":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. Sound and complete certificates for auantitative termination analysis of probabilistic programs. In: <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>. Vol 13371. Springer; 2022:55-78. doi:<a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">10.1007/978-3-031-13185-1_4</a>","apa":"Chatterjee, K., Goharshady, A. K., Meggendorfer, T., &#38; Zikelic, D. (2022). Sound and complete certificates for auantitative termination analysis of probabilistic programs. In <i>Proceedings of the 34th International Conference on Computer Aided Verification</i> (Vol. 13371, pp. 55–78). Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">https://doi.org/10.1007/978-3-031-13185-1_4</a>","short":"K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, in:, Proceedings of the 34th International Conference on Computer Aided Verification, Springer, 2022, pp. 55–78.","ista":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2022. Sound and complete certificates for auantitative termination analysis of probabilistic programs. Proceedings of the 34th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13371, 55–78.","mla":"Chatterjee, Krishnendu, et al. “Sound and Complete Certificates for Auantitative Termination Analysis of Probabilistic Programs.” <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>, vol. 13371, Springer, 2022, pp. 55–78, doi:<a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">10.1007/978-3-031-13185-1_4</a>.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. “Sound and Complete Certificates for Auantitative Termination Analysis of Probabilistic Programs.” In <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>, 13371:55–78. Springer, 2022. <a href=\"https://doi.org/10.1007/978-3-031-13185-1_4\">https://doi.org/10.1007/978-3-031-13185-1_4</a>."},"year":"2022","has_accepted_license":"1","month":"08","publication":"Proceedings of the 34th International Conference on Computer Aided Verification","ec_funded":1},{"day":"22","article_processing_charge":"No","volume":13411,"oa":1,"oa_version":"Preprint","doi":"10.1007/978-3-031-18283-9_17","status":"public","publication_status":"published","date_updated":"2025-09-10T09:48:15Z","publication":"Financial Cryptography and Data Security","month":"10","external_id":{"arxiv":["2110.08848"],"isi":["001423640200017"]},"year":"2022","citation":{"ama":"Avarikioti G, Pietrzak KZ, Salem I, Schmid S, Tiwari S, Yeo MX. Hide &#38; Seek: Privacy-preserving rebalancing on payment channel networks. In: <i>Financial Cryptography and Data Security</i>. Vol 13411. Springer Nature; 2022:358-373. doi:<a href=\"https://doi.org/10.1007/978-3-031-18283-9_17\">10.1007/978-3-031-18283-9_17</a>","apa":"Avarikioti, G., Pietrzak, K. Z., Salem, I., Schmid, S., Tiwari, S., &#38; Yeo, M. X. (2022). Hide &#38; Seek: Privacy-preserving rebalancing on payment channel networks. In <i>Financial Cryptography and Data Security</i> (Vol. 13411, pp. 358–373). Grenada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-18283-9_17\">https://doi.org/10.1007/978-3-031-18283-9_17</a>","short":"G. Avarikioti, K.Z. Pietrzak, I. Salem, S. Schmid, S. Tiwari, M.X. Yeo, in:, Financial Cryptography and Data Security, Springer Nature, 2022, pp. 358–373.","ista":"Avarikioti G, Pietrzak KZ, Salem I, Schmid S, Tiwari S, Yeo MX. 2022. Hide &#38; Seek: Privacy-preserving rebalancing on payment channel networks. Financial Cryptography and Data Security. FC: Financial Cryptography and Data Security, LNCS, vol. 13411, 358–373.","mla":"Avarikioti, Georgia, et al. “Hide &#38; Seek: Privacy-Preserving Rebalancing on Payment Channel Networks.” <i>Financial Cryptography and Data Security</i>, vol. 13411, Springer Nature, 2022, pp. 358–73, doi:<a href=\"https://doi.org/10.1007/978-3-031-18283-9_17\">10.1007/978-3-031-18283-9_17</a>.","chicago":"Avarikioti, Georgia, Krzysztof Z Pietrzak, Iosif Salem, Stefan Schmid, Samarth Tiwari, and Michelle X Yeo. “Hide &#38; Seek: Privacy-Preserving Rebalancing on Payment Channel Networks.” In <i>Financial Cryptography and Data Security</i>, 13411:358–73. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-18283-9_17\">https://doi.org/10.1007/978-3-031-18283-9_17</a>.","ieee":"G. Avarikioti, K. Z. Pietrzak, I. Salem, S. Schmid, S. Tiwari, and M. X. Yeo, “Hide &#38; Seek: Privacy-preserving rebalancing on payment channel networks,” in <i>Financial Cryptography and Data Security</i>, Grenada, 2022, vol. 13411, pp. 358–373."},"quality_controlled":"1","abstract":[{"lang":"eng","text":"Payment channels effectively move the transaction load off-chain thereby successfully addressing the inherent scalability problem most cryptocurrencies face. A major drawback of payment channels is the need to “top up” funds on-chain when a channel is depleted. Rebalancing was proposed to alleviate this issue, where parties with depleting channels move their funds along a cycle to replenish their channels off-chain. Protocols for rebalancing so far either introduce local solutions or compromise privacy.\r\nIn this work, we present an opt-in rebalancing protocol that is both private and globally optimal, meaning our protocol maximizes the total amount of rebalanced funds. We study rebalancing from the framework of linear programming. To obtain full privacy guarantees, we leverage multi-party computation in solving the linear program, which is executed by selected participants to maintain efficiency. Finally, we efficiently decompose the rebalancing solution into incentive-compatible cycles which conserve user balances when executed atomically."}],"department":[{"_id":"KrPi"}],"author":[{"last_name":"Avarikioti","id":"c20482a0-3b89-11eb-9862-88cf6404b88c","first_name":"Georgia","full_name":"Avarikioti, Georgia"},{"full_name":"Pietrzak, Krzysztof Z","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","first_name":"Krzysztof Z","orcid":"0000-0002-9139-1654","last_name":"Pietrzak"},{"full_name":"Salem, Iosif","last_name":"Salem","first_name":"Iosif"},{"last_name":"Schmid","first_name":"Stefan","full_name":"Schmid, Stefan"},{"first_name":"Samarth","last_name":"Tiwari","full_name":"Tiwari, Samarth"},{"id":"2D82B818-F248-11E8-B48F-1D18A9856A87","orcid":"0009-0001-3676-4809","first_name":"Michelle X","last_name":"Yeo","full_name":"Yeo, Michelle X"}],"title":"Hide & Seek: Privacy-preserving rebalancing on payment channel networks","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2110.08848"}],"publication_identifier":{"isbn":["9783031182822"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031182839"]},"arxiv":1,"type":"conference","date_published":"2022-10-22T00:00:00Z","page":"358-373","intvolume":"     13411","_id":"12167","alternative_title":["LNCS"],"scopus_import":"1","date_created":"2023-01-12T12:10:38Z","language":[{"iso":"eng"}],"conference":{"end_date":"2022-05-06","name":"FC: Financial Cryptography and Data Security","location":"Grenada","start_date":"2022-05-02"},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publisher":"Springer Nature","isi":1},{"external_id":{"isi":["001423640200013"],"arxiv":["2110.00960"]},"citation":{"ieee":"S. Cohen <i>et al.</i>, “Be aware of your leaders,” in <i>International Conference on Financial Cryptography and Data Security</i>, Grenada, 2022, vol. 13411, pp. 279–295.","ama":"Cohen S, Gelashvili R, Kokoris Kogias E, et al. Be aware of your leaders. In: <i>International Conference on Financial Cryptography and Data Security</i>. Vol 13411. Springer Nature; 2022:279-295. doi:<a href=\"https://doi.org/10.1007/978-3-031-18283-9_13\">10.1007/978-3-031-18283-9_13</a>","apa":"Cohen, S., Gelashvili, R., Kokoris Kogias, E., Li, Z., Malkhi, D., Sonnino, A., &#38; Spiegelman, A. (2022). Be aware of your leaders. In <i>International Conference on Financial Cryptography and Data Security</i> (Vol. 13411, pp. 279–295). Grenada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-18283-9_13\">https://doi.org/10.1007/978-3-031-18283-9_13</a>","chicago":"Cohen, Shir, Rati Gelashvili, Eleftherios Kokoris Kogias, Zekun Li, Dahlia Malkhi, Alberto Sonnino, and Alexander Spiegelman. “Be Aware of Your Leaders.” In <i>International Conference on Financial Cryptography and Data Security</i>, 13411:279–95. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-18283-9_13\">https://doi.org/10.1007/978-3-031-18283-9_13</a>.","mla":"Cohen, Shir, et al. “Be Aware of Your Leaders.” <i>International Conference on Financial Cryptography and Data Security</i>, vol. 13411, Springer Nature, 2022, pp. 279–95, doi:<a href=\"https://doi.org/10.1007/978-3-031-18283-9_13\">10.1007/978-3-031-18283-9_13</a>.","ista":"Cohen S, Gelashvili R, Kokoris Kogias E, Li Z, Malkhi D, Sonnino A, Spiegelman A. 2022. Be aware of your leaders. International Conference on Financial Cryptography and Data Security. FC: Financial Cryptography and Data Security, LNCS, vol. 13411, 279–295.","short":"S. Cohen, R. Gelashvili, E. Kokoris Kogias, Z. Li, D. Malkhi, A. Sonnino, A. Spiegelman, in:, International Conference on Financial Cryptography and Data Security, Springer Nature, 2022, pp. 279–295."},"year":"2022","month":"10","publication":"International Conference on Financial Cryptography and Data Security","date_updated":"2025-09-10T09:48:54Z","doi":"10.1007/978-3-031-18283-9_13","publication_status":"published","status":"public","oa":1,"oa_version":"Preprint","OA_type":"green","day":"22","article_processing_charge":"No","volume":13411,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publisher":"Springer Nature","isi":1,"conference":{"end_date":"2022-05-06","location":"Grenada","name":"FC: Financial Cryptography and Data Security","start_date":"2022-05-02"},"scopus_import":"1","OA_place":"repository","date_created":"2023-01-12T12:10:49Z","language":[{"iso":"eng"}],"date_published":"2022-10-22T00:00:00Z","page":"279-295","alternative_title":["LNCS"],"_id":"12168","intvolume":"     13411","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2110.00960"}],"arxiv":1,"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031182822"],"eisbn":["9783031182839"]},"type":"conference","title":"Be aware of your leaders","department":[{"_id":"ElKo"}],"author":[{"full_name":"Cohen, Shir","last_name":"Cohen","first_name":"Shir"},{"full_name":"Gelashvili, Rati","first_name":"Rati","last_name":"Gelashvili"},{"last_name":"Kokoris Kogias","first_name":"Eleftherios","id":"f5983044-d7ef-11ea-ac6d-fd1430a26d30","full_name":"Kokoris Kogias, Eleftherios"},{"last_name":"Li","first_name":"Zekun","full_name":"Li, Zekun"},{"full_name":"Malkhi, Dahlia","last_name":"Malkhi","first_name":"Dahlia"},{"last_name":"Sonnino","first_name":"Alberto","full_name":"Sonnino, Alberto"},{"last_name":"Spiegelman","first_name":"Alexander","full_name":"Spiegelman, Alexander"}],"quality_controlled":"1","abstract":[{"text":"Advances in blockchains have influenced the State-Machine-Replication (SMR) world and many state-of-the-art blockchain-SMR solutions are based on two pillars: Chaining and Leader-rotation. A predetermined round-robin mechanism used for Leader-rotation, however, has an undesirable behavior: crashed parties become designated leaders infinitely often, slowing down overall system performance. In this paper, we provide a new Leader-Aware SMR framework that, among other desirable properties, formalizes a Leader-utilization requirement that bounds the number of rounds whose leaders are faulty in crash-only executions.\r\nWe introduce Carousel, a novel, reputation-based Leader-rotation solution to achieve Leader-Aware SMR. The challenge in adaptive Leader-rotation is that it cannot rely on consensus to determine a leader, since consensus itself needs a leader. Carousel uses the available on-chain information to determine a leader locally and achieves Liveness despite this difficulty. A HotStuff implementation fitted with Carousel demonstrates drastic performance improvements: it increases throughput over 2x in faultless settings and provided a 20x throughput increase and 5x latency reduction in the presence of faults.","lang":"eng"}]},{"publisher":"Springer Nature","isi":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","conference":{"end_date":"2022-10-28","name":"ATVA: Automated Technology for Verification and Analysis","location":"Virtual","start_date":"2022-10-25"},"acknowledgement":"We thank Pranav Ashok and Maximilian Weininger for their contributions to spiritual predecessors of PET as well as motivating the initial development of this tool.","language":[{"iso":"eng"}],"scopus_import":"1","date_created":"2023-01-12T12:11:07Z","page":"320-326","intvolume":"     13505","_id":"12170","alternative_title":["LNCS"],"date_published":"2022-10-21T00:00:00Z","publication_identifier":{"isbn":["9783031199912"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031199929"]},"type":"conference","corr_author":"1","title":"PET – A partial exploration tool for probabilistic verification","author":[{"full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias","orcid":"0000-0002-1712-2165"}],"department":[{"_id":"KrCh"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"We present PET, a specialized and highly optimized framework for partial exploration on probabilistic systems. Over the last decade, several significant advances in the analysis of Markov decision processes employed partial exploration. In a nutshell, this idea allows to focus computation on specific parts of the system, guided by heuristics, while maintaining correctness. In particular, only relevant parts of the system are constructed on demand, which in turn potentially allows to omit constructing large parts of the system. Depending on the model, this leads to dramatic speed-ups, in extreme cases even up to an arbitrary factor. PET unifies several previous implementations and provides a flexible framework to easily implement partial exploration for many further problems. Our experimental evaluation shows significant improvements compared to the previous implementations while vastly reducing the overhead required to add support for additional properties."}],"external_id":{"isi":["001456146500020"]},"citation":{"ieee":"T. Meggendorfer, “PET – A partial exploration tool for probabilistic verification,” in <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, Virtual, 2022, vol. 13505, pp. 320–326.","chicago":"Meggendorfer, Tobias. “PET – A Partial Exploration Tool for Probabilistic Verification.” In <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, 13505:320–26. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">https://doi.org/10.1007/978-3-031-19992-9_20</a>.","mla":"Meggendorfer, Tobias. “PET – A Partial Exploration Tool for Probabilistic Verification.” <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 13505, Springer Nature, 2022, pp. 320–26, doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">10.1007/978-3-031-19992-9_20</a>.","short":"T. Meggendorfer, in:, 20th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2022, pp. 320–326.","ista":"Meggendorfer T. 2022. PET – A partial exploration tool for probabilistic verification. 20th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 13505, 320–326.","apa":"Meggendorfer, T. (2022). PET – A partial exploration tool for probabilistic verification. In <i>20th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 13505, pp. 320–326). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">https://doi.org/10.1007/978-3-031-19992-9_20</a>","ama":"Meggendorfer T. PET – A partial exploration tool for probabilistic verification. In: <i>20th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 13505. Springer Nature; 2022:320-326. doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">10.1007/978-3-031-19992-9_20</a>"},"year":"2022","publication":"20th International Symposium on Automated Technology for Verification and Analysis","month":"10","date_updated":"2025-09-10T09:49:29Z","doi":"10.1007/978-3-031-19992-9_20","publication_status":"published","status":"public","oa_version":"None","day":"21","article_processing_charge":"No","volume":13505},{"department":[{"_id":"ToHe"}],"author":[{"last_name":"Garcia Soto","orcid":"0000-0003-2936-5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","first_name":"Miriam","full_name":"Garcia Soto, Miriam"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"We propose an algorithmic approach for synthesizing linear hybrid automata from time-series data. Unlike existing approaches, our approach provides a whole family of models with the same discrete structure but different dynamics. Each model in the family is guaranteed to capture the input data up to a precision error ε, in the following sense: For each time series, the model contains an execution that is ε-close to the data points. Our construction allows to effectively choose a model from this family with minimal precision error ε. We demonstrate the algorithm’s efficiency and its ability to find precise models in two case studies."}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2208.06383","open_access":"1"}],"type":"conference","corr_author":"1","publication_identifier":{"isbn":["9783031199912"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031199929"]},"arxiv":1,"title":"Synthesis of parametric hybrid automata from time series","date_created":"2023-01-12T12:11:16Z","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement no. 847635, by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS.","date_published":"2022-10-21T00:00:00Z","alternative_title":["LNCS"],"_id":"12171","intvolume":"     13505","page":"337-353","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","isi":1,"publisher":"Springer Nature","conference":{"start_date":"2022-10-25","name":"ATVA: Automated Technology for Verification and Analysis","location":"Virtual","end_date":"2022-10-28"},"oa":1,"oa_version":"Preprint","volume":13505,"day":"21","article_processing_charge":"No","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"date_updated":"2025-09-10T09:50:08Z","publication_status":"published","status":"public","doi":"10.1007/978-3-031-19992-9_22","publication":"20th International Symposium on Automated Technology for Verification and Analysis","month":"10","ec_funded":1,"citation":{"ieee":"M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric hybrid automata from time series,” in <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, Virtual, 2022, vol. 13505, pp. 337–353.","apa":"Garcia Soto, M., Henzinger, T. A., &#38; Schilling, C. (2022). Synthesis of parametric hybrid automata from time series. In <i>20th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 13505, pp. 337–353). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">https://doi.org/10.1007/978-3-031-19992-9_22</a>","ama":"Garcia Soto M, Henzinger TA, Schilling C. Synthesis of parametric hybrid automata from time series. In: <i>20th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 13505. Springer Nature; 2022:337-353. doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">10.1007/978-3-031-19992-9_22</a>","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, 20th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2022, pp. 337–353.","mla":"Garcia Soto, Miriam, et al. “Synthesis of Parametric Hybrid Automata from Time Series.” <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">10.1007/978-3-031-19992-9_22</a>.","ista":"Garcia Soto M, Henzinger TA, Schilling C. 2022. Synthesis of parametric hybrid automata from time series. 20th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 13505, 337–353.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis of Parametric Hybrid Automata from Time Series.” In <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, 13505:337–53. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">https://doi.org/10.1007/978-3-031-19992-9_22</a>."},"year":"2022","external_id":{"isi":["001456146500022"],"arxiv":["2208.06383"]}},{"ec_funded":1,"publication":"16th International Conference on Reachability Problems","month":"10","citation":{"ieee":"S. Bose, T. A. Henzinger, K. Lehtinen, S. Schewe, and P. Totzke, “History-deterministic timed automata are not determinizable,” in <i>16th International Conference on Reachability Problems</i>, Kaiserslautern, Germany, 2022, vol. 13608, pp. 67–76.","chicago":"Bose, Sougata, Thomas A Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke. “History-Deterministic Timed Automata Are Not Determinizable.” In <i>16th International Conference on Reachability Problems</i>, 13608:67–76. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-19135-0_5\">https://doi.org/10.1007/978-3-031-19135-0_5</a>.","short":"S. Bose, T.A. Henzinger, K. Lehtinen, S. Schewe, P. Totzke, in:, 16th International Conference on Reachability Problems, Springer Nature, 2022, pp. 67–76.","ista":"Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. 2022. History-deterministic timed automata are not determinizable. 16th International Conference on Reachability Problems. RC: Reachability Problems, LNCS, vol. 13608, 67–76.","mla":"Bose, Sougata, et al. “History-Deterministic Timed Automata Are Not Determinizable.” <i>16th International Conference on Reachability Problems</i>, vol. 13608, Springer Nature, 2022, pp. 67–76, doi:<a href=\"https://doi.org/10.1007/978-3-031-19135-0_5\">10.1007/978-3-031-19135-0_5</a>.","ama":"Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. History-deterministic timed automata are not determinizable. In: <i>16th International Conference on Reachability Problems</i>. Vol 13608. Springer Nature; 2022:67-76. doi:<a href=\"https://doi.org/10.1007/978-3-031-19135-0_5\">10.1007/978-3-031-19135-0_5</a>","apa":"Bose, S., Henzinger, T. A., Lehtinen, K., Schewe, S., &#38; Totzke, P. (2022). History-deterministic timed automata are not determinizable. In <i>16th International Conference on Reachability Problems</i> (Vol. 13608, pp. 67–76). Kaiserslautern, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-19135-0_5\">https://doi.org/10.1007/978-3-031-19135-0_5</a>"},"year":"2022","external_id":{"isi":["001333698300005"]},"volume":13608,"day":"12","article_processing_charge":"No","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"oa":1,"oa_version":"Preprint","publication_status":"published","status":"public","doi":"10.1007/978-3-031-19135-0_5","date_updated":"2025-09-10T09:50:45Z","date_published":"2022-10-12T00:00:00Z","intvolume":"     13608","_id":"12175","alternative_title":["LNCS"],"page":"67-76","date_created":"2023-01-12T12:11:57Z","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, the EPSRC project EP/V025848/1, and the EPSRC project EP/X017796/1.","conference":{"end_date":"2022-10-21","start_date":"2022-10-17","location":"Kaiserslautern, Germany","name":"RC: Reachability Problems"},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","isi":1,"publisher":"Springer Nature","quality_controlled":"1","abstract":[{"text":"An automaton is history-deterministic (HD) if one can safely resolve its non-deterministic choices on the fly. In a recent paper, Henzinger, Lehtinen and Totzke studied this in the context of Timed Automata [9], where it was conjectured that the class of timed ω-languages recognised by HD-timed automata strictly extends that of deterministic ones. We provide a proof for this fact.","lang":"eng"}],"department":[{"_id":"ToHe"}],"author":[{"first_name":"Sougata","last_name":"Bose","full_name":"Bose, Sougata"},{"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":"Lehtinen, Karoliina","first_name":"Karoliina","last_name":"Lehtinen"},{"full_name":"Schewe, Sven","first_name":"Sven","last_name":"Schewe"},{"full_name":"Totzke, Patrick","first_name":"Patrick","last_name":"Totzke"}],"title":"History-deterministic timed automata are not determinizable","main_file_link":[{"open_access":"1","url":"https://hal.science/hal-03849398/"}],"type":"conference","publication_identifier":{"isbn":["9783031191343"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031191350"]}},{"publication":"Advances in Cryptology – CRYPTO 2022","month":"10","external_id":{"isi":["000886792700013"]},"citation":{"ieee":"C. Hoffmann, P. Hubáček, C. Kamath, K. Klein, and K. Z. Pietrzak, “Practical statistically-sound proofs of exponentiation in any group,” in <i>Advances in Cryptology – CRYPTO 2022</i>, Santa Barbara, CA, United States, 2022, vol. 13508, pp. 370–399.","ama":"Hoffmann C, Hubáček P, Kamath C, Klein K, Pietrzak KZ. Practical statistically-sound proofs of exponentiation in any group. In: <i>Advances in Cryptology – CRYPTO 2022</i>. Vol 13508. Springer Nature; 2022:370-399. doi:<a href=\"https://doi.org/10.1007/978-3-031-15979-4_13\">10.1007/978-3-031-15979-4_13</a>","apa":"Hoffmann, C., Hubáček, P., Kamath, C., Klein, K., &#38; Pietrzak, K. Z. (2022). Practical statistically-sound proofs of exponentiation in any group. In <i>Advances in Cryptology – CRYPTO 2022</i> (Vol. 13508, pp. 370–399). Santa Barbara, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-15979-4_13\">https://doi.org/10.1007/978-3-031-15979-4_13</a>","chicago":"Hoffmann, Charlotte, Pavel Hubáček, Chethan Kamath, Karen Klein, and Krzysztof Z Pietrzak. “Practical Statistically-Sound Proofs of Exponentiation in Any Group.” In <i>Advances in Cryptology – CRYPTO 2022</i>, 13508:370–99. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-15979-4_13\">https://doi.org/10.1007/978-3-031-15979-4_13</a>.","short":"C. Hoffmann, P. Hubáček, C. Kamath, K. Klein, K.Z. Pietrzak, in:, Advances in Cryptology – CRYPTO 2022, Springer Nature, 2022, pp. 370–399.","ista":"Hoffmann C, Hubáček P, Kamath C, Klein K, Pietrzak KZ. 2022. Practical statistically-sound proofs of exponentiation in any group. Advances in Cryptology – CRYPTO 2022. CRYPTO: International Cryptology Conference, LNCS, vol. 13508, 370–399.","mla":"Hoffmann, Charlotte, et al. “Practical Statistically-Sound Proofs of Exponentiation in Any Group.” <i>Advances in Cryptology – CRYPTO 2022</i>, vol. 13508, Springer Nature, 2022, pp. 370–99, doi:<a href=\"https://doi.org/10.1007/978-3-031-15979-4_13\">10.1007/978-3-031-15979-4_13</a>."},"year":"2022","day":"13","article_processing_charge":"No","volume":13508,"oa_version":"Preprint","oa":1,"doi":"10.1007/978-3-031-15979-4_13","status":"public","publication_status":"published","date_updated":"2026-04-07T12:34:30Z","page":"370-399","_id":"12176","intvolume":"     13508","alternative_title":["LNCS"],"date_published":"2022-10-13T00:00:00Z","acknowledgement":"We would like to thank the authors of [BHR+21] for clarifying several questions we had\r\nregarding their results. Pavel Hubá£ek was supported by the Grant Agency of the Czech\r\nRepublic under the grant agreement no. 19-27871X and by the Charles University project\r\nUNCE/SCI/004. Chethan Kamath is supported by Azrieli International Postdoctoral Fellowship\r\nand ISF grants 484/18 and 1789/19. Karen Klein was supported in part by ERC CoG grant\r\n724307 and conducted part of this work at Institute of Science and Technology Austria.","language":[{"iso":"eng"}],"scopus_import":"1","date_created":"2023-01-12T12:12:07Z","conference":{"name":"CRYPTO: International Cryptology Conference","location":"Santa Barbara, CA, United States","start_date":"2022-08-15","end_date":"2022-08-18"},"publisher":"Springer Nature","isi":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","abstract":[{"text":"A proof of exponentiation (PoE) in a group G of unknown order allows a prover to convince a verifier that a tuple (x,q,T,y)∈G×N×N×G satisfies xqT=y. This primitive has recently found exciting applications in the constructions of verifiable delay functions and succinct arguments of knowledge. The most practical PoEs only achieve soundness either under computational assumptions, i.e., they are arguments (Wesolowski, Journal of Cryptology 2020), or in groups that come with the promise of not having any small subgroups (Pietrzak, ITCS 2019). The only statistically-sound PoE in general groups of unknown order is due to Block et al. (CRYPTO 2021), and can be seen as an elaborate parallel repetition of Pietrzak’s PoE: to achieve λ bits of security, say λ=80, the number of repetitions required (and thus the blow-up in communication) is as large as λ.\r\n\r\nIn this work, we propose a statistically-sound PoE for the case where the exponent q is the product of all primes up to some bound B. We show that, in this case, it suffices to run only λ/log(B) parallel instances of Pietrzak’s PoE, which reduces the concrete proof-size compared to Block et al. by an order of magnitude. Furthermore, we show that in the known applications where PoEs are used as a building block such structured exponents are viable. Finally, we also discuss batching of our PoE, showing that many proofs (for the same G and q but different x and T) can be batched by adding only a single element to the proof per additional statement.","lang":"eng"}],"author":[{"full_name":"Hoffmann, Charlotte","last_name":"Hoffmann","first_name":"Charlotte","orcid":"0000-0003-2027-5549","id":"0f78d746-dc7d-11ea-9b2f-83f92091afe7"},{"full_name":"Hubáček, Pavel","first_name":"Pavel","last_name":"Hubáček"},{"first_name":"Chethan","last_name":"Kamath","full_name":"Kamath, Chethan"},{"full_name":"Klein, Karen","last_name":"Klein","first_name":"Karen"},{"full_name":"Pietrzak, Krzysztof Z","last_name":"Pietrzak","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9139-1654","first_name":"Krzysztof Z"}],"department":[{"_id":"KrPi"}],"title":"Practical statistically-sound proofs of exponentiation in any group","related_material":{"record":[{"id":"20920","status":"public","relation":"dissertation_contains"},{"id":"20556","status":"public","relation":"dissertation_contains"}]},"publication_identifier":{"eisbn":["9783031159794"],"isbn":["9783031159787"],"issn":["0302-9743"],"eissn":["1611-3349"]},"corr_author":"1","type":"conference","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2022/1021"}]},{"month":"10","publication":"Financial Cryptography and Data Security","citation":{"ieee":"R. Gelashvili, E. Kokoris Kogias, A. Sonnino, A. Spiegelman, and Z. Xiang, “Jolteon and ditto: Network-adaptive efficient consensus with asynchronous fallback,” in <i>Financial Cryptography and Data Security</i>, Radisson Grenada Beach Resort, Grenada, 2022, vol. 13411, pp. 296–315.","apa":"Gelashvili, R., Kokoris Kogias, E., Sonnino, A., Spiegelman, A., &#38; Xiang, Z. (2022). Jolteon and ditto: Network-adaptive efficient consensus with asynchronous fallback. In <i>Financial Cryptography and Data Security</i> (Vol. 13411, pp. 296–315). Radisson Grenada Beach Resort, Grenada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-18283-9_14\">https://doi.org/10.1007/978-3-031-18283-9_14</a>","ama":"Gelashvili R, Kokoris Kogias E, Sonnino A, Spiegelman A, Xiang Z. Jolteon and ditto: Network-adaptive efficient consensus with asynchronous fallback. In: <i>Financial Cryptography and Data Security</i>. Vol 13411. Springer Nature; 2022:296-315. doi:<a href=\"https://doi.org/10.1007/978-3-031-18283-9_14\">10.1007/978-3-031-18283-9_14</a>","mla":"Gelashvili, Rati, et al. “Jolteon and Ditto: Network-Adaptive Efficient Consensus with Asynchronous Fallback.” <i>Financial Cryptography and Data Security</i>, vol. 13411, Springer Nature, 2022, pp. 296–315, doi:<a href=\"https://doi.org/10.1007/978-3-031-18283-9_14\">10.1007/978-3-031-18283-9_14</a>.","short":"R. Gelashvili, E. Kokoris Kogias, A. Sonnino, A. Spiegelman, Z. Xiang, in:, Financial Cryptography and Data Security, Springer Nature, 2022, pp. 296–315.","ista":"Gelashvili R, Kokoris Kogias E, Sonnino A, Spiegelman A, Xiang Z. 2022. Jolteon and ditto: Network-adaptive efficient consensus with asynchronous fallback. Financial Cryptography and Data Security. FC: Financial Cryptography, LNCS, vol. 13411, 296–315.","chicago":"Gelashvili, Rati, Eleftherios Kokoris Kogias, Alberto Sonnino, Alexander Spiegelman, and Zhuolun Xiang. “Jolteon and Ditto: Network-Adaptive Efficient Consensus with Asynchronous Fallback.” In <i>Financial Cryptography and Data Security</i>, 13411:296–315. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-18283-9_14\">https://doi.org/10.1007/978-3-031-18283-9_14</a>."},"year":"2022","external_id":{"arxiv":["2106.10362"],"isi":["001423640200014"]},"oa":1,"oa_version":"Preprint","volume":13411,"article_processing_charge":"No","day":"22","date_updated":"2025-09-10T09:52:23Z","status":"public","publication_status":"published","doi":"10.1007/978-3-031-18283-9_14","date_created":"2023-01-16T10:05:51Z","scopus_import":"1","language":[{"iso":"eng"}],"acknowledgement":"We thank our shepherd Aniket Kate and the anonymous reviewers at FC 2022 for their helpful feedback. This work is supported by the Novi team at Facebook. We also thank the Novi Research and Engineering teams for valuable feedback, and in particular Mathieu Baudet, Andrey Chursin, George Danezis, Zekun Li, and Dahlia Malkhi for discussions that shaped this work.","date_published":"2022-10-22T00:00:00Z","intvolume":"     13411","_id":"12298","alternative_title":["LNCS"],"page":"296-315","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","isi":1,"publisher":"Springer Nature","conference":{"end_date":"2022-05-06","name":"FC: Financial Cryptography","location":"Radisson Grenada Beach Resort, Grenada","start_date":"2022-05-02"},"department":[{"_id":"ElKo"}],"author":[{"full_name":"Gelashvili, Rati","first_name":"Rati","last_name":"Gelashvili"},{"full_name":"Kokoris Kogias, Eleftherios","id":"f5983044-d7ef-11ea-ac6d-fd1430a26d30","first_name":"Eleftherios","last_name":"Kokoris Kogias"},{"full_name":"Sonnino, Alberto","first_name":"Alberto","last_name":"Sonnino"},{"full_name":"Spiegelman, Alexander","last_name":"Spiegelman","first_name":"Alexander"},{"full_name":"Xiang, Zhuolun","first_name":"Zhuolun","last_name":"Xiang"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"Existing committee-based Byzantine state machine replication (SMR) protocols, typically deployed in production blockchains, face a clear trade-off: (1) they either achieve linear communication cost in the steady state, but sacrifice liveness during periods of asynchrony, or (2) they are robust (progress with probability one) but pay quadratic communication cost. We believe this trade-off is unwarranted since existing linear protocols still have asymptotic quadratic cost in the worst case. We design Ditto, a Byzantine SMR protocol that enjoys the best of both worlds: optimal communication on and off the steady state (linear and quadratic, respectively) and progress guarantee under asynchrony and DDoS attacks. We achieve this by replacing the view-synchronization of partially synchronous protocols with an asynchronous fallback mechanism at no extra asymptotic cost. Specifically, we start from HotStuff, a state-of-the-art linear protocol, and gradually build Ditto. As a separate contribution and an intermediate step, we design a 2-chain version of HotStuff, Jolteon, which leverages a quadratic view-change mechanism to reduce the latency of the standard 3-chain HotStuff. We implement and experimentally evaluate all our systems to prove that breaking the robustness-efficiency trade-off is in the realm of practicality."}],"main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.2106.10362"}],"type":"conference","publication_identifier":{"eisbn":["9783031182839"],"isbn":["9783031182822"],"eissn":["1611-3349"],"issn":["0302-9743"]},"arxiv":1,"title":"Jolteon and ditto: Network-adaptive efficient consensus with asynchronous fallback"},{"ddc":["000"],"doi":"10.1007/978-3-031-13188-2_6","publication_status":"published","status":"public","date_updated":"2025-04-14T07:55:56Z","article_processing_charge":"No","day":"06","volume":13372,"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"file":[{"file_size":497682,"date_updated":"2023-01-30T12:51:02Z","creator":"dernst","content_type":"application/pdf","file_id":"12465","file_name":"2022_LNCS_Doveri.pdf","success":1,"date_created":"2023-01-30T12:51:02Z","relation":"main_file","checksum":"edc363b1be5447a09063e115c247918a","access_level":"open_access"}],"file_date_updated":"2023-01-30T12:51:02Z","oa":1,"oa_version":"Published Version","has_accepted_license":"1","external_id":{"isi":["000870310500006"],"arxiv":["2207.13549"]},"year":"2022","citation":{"chicago":"Doveri, Kyveli, Pierre Ganty, and Nicolas Adrien Mazzocchi. “FORQ-Based Language Inclusion Formal Testing.” In <i>Computer Aided Verification</i>, 13372:109–29. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-13188-2_6\">https://doi.org/10.1007/978-3-031-13188-2_6</a>.","ista":"Doveri K, Ganty P, Mazzocchi NA. 2022. FORQ-based language inclusion formal testing. Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13372, 109–129.","mla":"Doveri, Kyveli, et al. “FORQ-Based Language Inclusion Formal Testing.” <i>Computer Aided Verification</i>, vol. 13372, Springer Nature, 2022, pp. 109–29, doi:<a href=\"https://doi.org/10.1007/978-3-031-13188-2_6\">10.1007/978-3-031-13188-2_6</a>.","short":"K. Doveri, P. Ganty, N.A. Mazzocchi, in:, Computer Aided Verification, Springer Nature, 2022, pp. 109–129.","apa":"Doveri, K., Ganty, P., &#38; Mazzocchi, N. A. (2022). FORQ-based language inclusion formal testing. In <i>Computer Aided Verification</i> (Vol. 13372, pp. 109–129). Haifa, Israel: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-13188-2_6\">https://doi.org/10.1007/978-3-031-13188-2_6</a>","ama":"Doveri K, Ganty P, Mazzocchi NA. FORQ-based language inclusion formal testing. In: <i>Computer Aided Verification</i>. Vol 13372. Springer Nature; 2022:109-129. doi:<a href=\"https://doi.org/10.1007/978-3-031-13188-2_6\">10.1007/978-3-031-13188-2_6</a>","ieee":"K. Doveri, P. Ganty, and N. A. Mazzocchi, “FORQ-based language inclusion formal testing,” in <i>Computer Aided Verification</i>, Haifa, Israel, 2022, vol. 13372, pp. 109–129."},"ec_funded":1,"month":"08","publication":"Computer Aided Verification","title":"FORQ-based language inclusion formal testing","publication_identifier":{"isbn":["9783031131875"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031131882"]},"arxiv":1,"type":"conference","abstract":[{"text":"We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the Büchi automaton to the right of the inclusion sign. The resulting implementation, called FORKLIFT, scales up better than the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870","lang":"eng"}],"quality_controlled":"1","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"ToHe"}],"author":[{"full_name":"Doveri, Kyveli","first_name":"Kyveli","last_name":"Doveri"},{"last_name":"Ganty","first_name":"Pierre","full_name":"Ganty, Pierre"},{"first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien"}],"conference":{"location":"Haifa, Israel","name":"CAV: Computer Aided Verification","start_date":"2022-08-07","end_date":"2022-08-10"},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publisher":"Springer Nature","isi":1,"date_published":"2022-08-06T00:00:00Z","page":"109-129","alternative_title":["LNCS"],"_id":"12302","intvolume":"     13372","scopus_import":"1","date_created":"2023-01-16T10:06:31Z","acknowledgement":"This work was partially funded by the ESF Investing in your future, the Madrid regional project S2018/TCS-4339 BLOQUES, the Spanish project PGC2018-102210-B-I00 BOSCO, the Ramón y Cajal fellowship RYC-2016-20281, and the ERC grant PR1001ERC02.","language":[{"iso":"eng"}]}]