[{"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"https://eprint.iacr.org/2023/238","open_access":"1"}],"oa":1,"publication_identifier":{"isbn":["9783031313677"],"eissn":["1611-3349"],"issn":["0302-9743"]},"type":"conference","date_published":"2023-05-02T00:00:00Z","conference":{"location":"Atlanta, GA, United States","end_date":"2023-05-10","name":"PKC: Public-Key Cryptography","start_date":"2023-05-07"},"language":[{"iso":"eng"}],"month":"05","oa_version":"Submitted Version","publication":"Public-Key Cryptography - PKC 2023","acknowledgement":"We are grateful to Pavel Atnashev for clarifying via e-mail several aspects of the primality tests implementated in the PrimeGrid project. Pavel Hubáček is supported by the Czech Academy of Sciences (RVO 67985840), the Grant Agency of the Czech Republic under the grant agreement no. 19-27871X, and by the Charles University project UNCE/SCI/004. Chethan Kamath is supported by Azrieli International Postdoctoral Fellowship, ISF grants 484/18 and 1789/19, and ERC StG project SPP: Secrecy Preserving Proofs.","volume":13940,"abstract":[{"lang":"eng","text":"GIMPS and PrimeGrid are large-scale distributed projects dedicated to searching giant prime numbers, usually of special forms like Mersenne and Proth primes. The numbers in the current search-space are millions of digits large and the participating volunteers need to run resource-consuming primality tests. Once a candidate prime N has been found, the only way for another party to independently verify the primality of N used to be by repeating the expensive primality test. To avoid the need for second recomputation of each primality test, these projects have recently adopted certifying mechanisms that enable efficient verification of performed tests. However, the mechanisms presently in place only detect benign errors and there is no guarantee against adversarial behavior: a malicious volunteer can mislead the project to reject a giant prime as being non-prime.\r\nIn this paper, we propose a practical, cryptographically-sound mechanism for certifying the non-primality of Proth numbers. That is, a volunteer can – parallel to running the primality test for N – generate an efficiently verifiable proof at a little extra cost certifying that N is not prime. The interactive protocol has statistical soundness and can be made non-interactive using the Fiat-Shamir heuristic.\r\nOur approach is based on a cryptographic primitive called Proof of Exponentiation (PoE) which, for a group G, certifies that a tuple (x,y,T)∈G2×N satisfies x2T=y (Pietrzak, ITCS 2019 and Wesolowski, J. Cryptol. 2020). In particular, we show how to adapt Pietrzak’s PoE at a moderate additional cost to make it a cryptographically-sound certificate of non-primality."}],"day":"02","doi":"10.1007/978-3-031-31368-4_19","year":"2023","citation":{"chicago":"Hoffmann, Charlotte, Pavel Hubáček, Chethan Kamath, and Krzysztof Z Pietrzak. “Certifying Giant Nonprimes.” In <i>Public-Key Cryptography - PKC 2023</i>, 13940:530–53. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-31368-4_19\">https://doi.org/10.1007/978-3-031-31368-4_19</a>.","ieee":"C. Hoffmann, P. Hubáček, C. Kamath, and K. Z. Pietrzak, “Certifying giant nonprimes,” in <i>Public-Key Cryptography - PKC 2023</i>, Atlanta, GA, United States, 2023, vol. 13940, pp. 530–553.","apa":"Hoffmann, C., Hubáček, P., Kamath, C., &#38; Pietrzak, K. Z. (2023). Certifying giant nonprimes. In <i>Public-Key Cryptography - PKC 2023</i> (Vol. 13940, pp. 530–553). Atlanta, GA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-31368-4_19\">https://doi.org/10.1007/978-3-031-31368-4_19</a>","ama":"Hoffmann C, Hubáček P, Kamath C, Pietrzak KZ. Certifying giant nonprimes. In: <i>Public-Key Cryptography - PKC 2023</i>. Vol 13940. Springer Nature; 2023:530-553. doi:<a href=\"https://doi.org/10.1007/978-3-031-31368-4_19\">10.1007/978-3-031-31368-4_19</a>","ista":"Hoffmann C, Hubáček P, Kamath C, Pietrzak KZ. 2023. Certifying giant nonprimes. Public-Key Cryptography - PKC 2023. PKC: Public-Key Cryptography, LNCS, vol. 13940, 530–553.","mla":"Hoffmann, Charlotte, et al. “Certifying Giant Nonprimes.” <i>Public-Key Cryptography - PKC 2023</i>, vol. 13940, Springer Nature, 2023, pp. 530–53, doi:<a href=\"https://doi.org/10.1007/978-3-031-31368-4_19\">10.1007/978-3-031-31368-4_19</a>.","short":"C. Hoffmann, P. Hubáček, C. Kamath, K.Z. Pietrzak, in:, Public-Key Cryptography - PKC 2023, Springer Nature, 2023, pp. 530–553."},"date_updated":"2023-06-19T08:03:37Z","publisher":"Springer Nature","quality_controlled":"1","page":"530-553","intvolume":"     13940","title":"Certifying giant nonprimes","alternative_title":["LNCS"],"department":[{"_id":"KrPi"}],"date_created":"2023-06-18T22:00:47Z","article_processing_charge":"No","publication_status":"published","author":[{"id":"0f78d746-dc7d-11ea-9b2f-83f92091afe7","full_name":"Hoffmann, Charlotte","first_name":"Charlotte","last_name":"Hoffmann"},{"first_name":"Pavel","last_name":"Hubáček","full_name":"Hubáček, Pavel"},{"last_name":"Kamath","first_name":"Chethan","full_name":"Kamath, Chethan"},{"id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","first_name":"Krzysztof Z","last_name":"Pietrzak","orcid":"0000-0002-9139-1654","full_name":"Pietrzak, Krzysztof Z"}],"scopus_import":"1","_id":"13143"},{"project":[{"_id":"bd9ca328-d553-11ed-ba76-dc4f890cfe62","call_identifier":"H2020","name":"The design and evaluation of modern fully dynamic data structures","grant_number":"101019564"},{"grant_number":"P33775 ","name":"Fast Algorithms for a Reactive Network Layer","_id":"bd9e3a2e-d553-11ed-ba76-8aa684ce17fe"}],"oa_version":"Preprint","month":"05","publication":"International Conference on Integer Programming and Combinatorial Optimization","conference":{"location":"Madison, WI, United States","end_date":"2023-06-23","start_date":"2023-06-21","name":"IPCO: Integer Programming and Combinatorial Optimization"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031327254"]},"oa":1,"type":"conference","date_published":"2023-05-22T00:00:00Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2301.09217","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","date_created":"2023-07-16T22:01:11Z","department":[{"_id":"MoHe"}],"article_processing_charge":"No","publication_status":"published","intvolume":"     13904","alternative_title":["LNCS"],"title":"Multiplicative auction algorithm for approximate maximum weight bipartite matching","scopus_import":"1","_id":"13236","author":[{"first_name":"Da Wei","last_name":"Zheng","full_name":"Zheng, Da Wei"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","first_name":"Monika H","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530"}],"publisher":"Springer Nature","ec_funded":1,"quality_controlled":"1","page":"453-465","day":"22","doi":"10.1007/978-3-031-32726-1_32","arxiv":1,"abstract":[{"lang":"eng","text":"We present an auction algorithm using multiplicative instead of constant weight updates to compute a (1−ε)-approximate maximum weight matching (MWM) in a bipartite graph with n vertices and m edges in time O(mε−1log(ε−1)), matching the running time of the linear-time approximation algorithm of Duan and Pettie [JACM ’14]. Our algorithm is very simple and it can be extended to give a dynamic data structure that maintains a (1−ε)-approximate maximum weight matching under (1) one-sided vertex deletions (with incident edges) and (2) one-sided vertex insertions (with incident edges sorted by weight) to the other side. The total time time used is O(mε−1log(ε−1)), where m is the sum of the number of initially existing and inserted edges."}],"year":"2023","citation":{"ieee":"D. W. Zheng and M. H. Henzinger, “Multiplicative auction algorithm for approximate maximum weight bipartite matching,” in <i>International Conference on Integer Programming and Combinatorial Optimization</i>, Madison, WI, United States, 2023, vol. 13904, pp. 453–465.","chicago":"Zheng, Da Wei, and Monika H Henzinger. “Multiplicative Auction Algorithm for Approximate Maximum Weight Bipartite Matching.” In <i>International Conference on Integer Programming and Combinatorial Optimization</i>, 13904:453–65. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-32726-1_32\">https://doi.org/10.1007/978-3-031-32726-1_32</a>.","ama":"Zheng DW, Henzinger MH. Multiplicative auction algorithm for approximate maximum weight bipartite matching. In: <i>International Conference on Integer Programming and Combinatorial Optimization</i>. Vol 13904. Springer Nature; 2023:453-465. doi:<a href=\"https://doi.org/10.1007/978-3-031-32726-1_32\">10.1007/978-3-031-32726-1_32</a>","apa":"Zheng, D. W., &#38; Henzinger, M. H. (2023). Multiplicative auction algorithm for approximate maximum weight bipartite matching. In <i>International Conference on Integer Programming and Combinatorial Optimization</i> (Vol. 13904, pp. 453–465). Madison, WI, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-32726-1_32\">https://doi.org/10.1007/978-3-031-32726-1_32</a>","ista":"Zheng DW, Henzinger MH. 2023. Multiplicative auction algorithm for approximate maximum weight bipartite matching. International Conference on Integer Programming and Combinatorial Optimization. IPCO: Integer Programming and Combinatorial Optimization, LNCS, vol. 13904, 453–465.","mla":"Zheng, Da Wei, and Monika H. Henzinger. “Multiplicative Auction Algorithm for Approximate Maximum Weight Bipartite Matching.” <i>International Conference on Integer Programming and Combinatorial Optimization</i>, vol. 13904, Springer Nature, 2023, pp. 453–65, doi:<a href=\"https://doi.org/10.1007/978-3-031-32726-1_32\">10.1007/978-3-031-32726-1_32</a>.","short":"D.W. Zheng, M.H. Henzinger, in:, International Conference on Integer Programming and Combinatorial Optimization, Springer Nature, 2023, pp. 453–465."},"date_updated":"2023-07-18T07:08:51Z","external_id":{"arxiv":["2301.09217"]},"volume":13904,"acknowledgement":"The first author thanks to Chandra Chekuri for useful discussions about this paper. This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 101019564 “The Design of Modern Fully Dynamic Data Structures (MoDynStruct)” and from the Austrian Science Fund (FWF) project “Fast Algorithms for a Reactive Network Layer (ReactNet)”, P 33775-N, with additional funding from the netidee SCIENCE Stiftung, 2020–2024."},{"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2204.13459","open_access":"1"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"relation":"dissertation_contains","id":"14506","status":"public"}]},"type":"conference","date_published":"2023-05-25T00:00:00Z","publication_identifier":{"isbn":["9783031327322"],"issn":["0302-9743"],"eissn":["1611-3349"]},"oa":1,"language":[{"iso":"eng"}],"conference":{"name":"SIROCCO: Structural Information and Communication Complexity","start_date":"2023-06-06","end_date":"2023-06-09","location":"Alcala de Henares, Spain"},"publication":"SIROCCO 2023: Structural Information and Communication Complexity ","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"oa_version":"Preprint","month":"05","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.","volume":13892,"year":"2023","citation":{"short":"S. Schmid, J. Svoboda, M.X. Yeo, in:, SIROCCO 2023: Structural Information and Communication Complexity , Springer Nature, 2023, pp. 576–594.","mla":"Schmid, Stefan, et al. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” <i>SIROCCO 2023: 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 packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. SIROCCO 2023: Structural Information and Communication Complexity . SIROCCO: Structural Information and Communication Complexity, LNCS, vol. 13892, 576–594.","apa":"Schmid, S., Svoboda, J., &#38; Yeo, M. X. (2023). Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. In <i>SIROCCO 2023: Structural Information and Communication Complexity </i> (Vol. 13892, pp. 576–594). Alcala 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 packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation. In: <i>SIROCCO 2023: 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>","ieee":"S. Schmid, J. Svoboda, and M. X. Yeo, “Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation,” in <i>SIROCCO 2023: Structural Information and Communication Complexity </i>, Alcala de Henares, Spain, 2023, vol. 13892, pp. 576–594.","chicago":"Schmid, Stefan, Jakub Svoboda, and Michelle X Yeo. “Weighted Packet Selection for Rechargeable Links in Cryptocurrency Networks: Complexity and Approximation.” In <i>SIROCCO 2023: 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>."},"date_updated":"2025-07-14T09:09:53Z","external_id":{"arxiv":["2204.13459"]},"day":"25","arxiv":1,"doi":"10.1007/978-3-031-32733-9_26","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+ε)⋅(1+3–√) for some arbitrary ε>0.\r\n."}],"ec_funded":1,"quality_controlled":"1","page":"576-594","publisher":"Springer Nature","scopus_import":"1","_id":"13238","author":[{"last_name":"Schmid","first_name":"Stefan","full_name":"Schmid, Stefan"},{"first_name":"Jakub","last_name":"Svoboda","orcid":"0000-0002-1419-3267","full_name":"Svoboda, Jakub","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"},{"id":"2D82B818-F248-11E8-B48F-1D18A9856A87","last_name":"Yeo","first_name":"Michelle X","full_name":"Yeo, Michelle X","orcid":"0009-0001-3676-4809"}],"department":[{"_id":"KrPi"},{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2023-07-16T22:01:12Z","publication_status":"published","intvolume":"     13892","alternative_title":["LNCS"],"title":"Weighted packet selection for rechargeable links in cryptocurrency networks: Complexity and approximation"},{"language":[{"iso":"eng"}],"conference":{"name":"CAV: Computer Aided Verification","start_date":"2023-07-17","end_date":"2023-07-22","location":"Paris, France"},"has_accepted_license":"1","publication":"Computer Aided Verification","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"oa_version":"Published Version","month":"07","file":[{"creator":"dernst","file_id":"13327","access_level":"open_access","relation":"main_file","success":1,"content_type":"application/pdf","file_name":"2023_LNCS_CAV_HenzingerT.pdf","date_updated":"2023-07-31T08:11:20Z","checksum":"ccaf94bf7d658ba012c016e11869b54c","file_size":647760,"date_created":"2023-07-31T08:11:20Z"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2023-07-18T00:00:00Z","publication_identifier":{"eisbn":["9783031377037"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031377020"]},"oa":1,"quality_controlled":"1","ec_funded":1,"page":"358–382","file_date_updated":"2023-07-31T08:11:20Z","publisher":"Springer Nature","_id":"13310","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"},{"id":"f1dedef5-2f78-11ee-989a-c4c97bccf506","full_name":"Karimi, Mahyar","orcid":"0009-0005-0820-1696","last_name":"Karimi","first_name":"Mahyar"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542","last_name":"Kueffner","first_name":"Konstantin"},{"full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"}],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"article_processing_charge":"Yes (in subscription journal)","date_created":"2023-07-25T18:32:40Z","publication_status":"published","intvolume":"     13965","alternative_title":["LNCS"],"title":"Monitoring algorithmic fairness","volume":13965,"acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG101020093.","ddc":["000"],"year":"2023","citation":{"apa":"Henzinger, T. A., Karimi, M., Kueffner, K., &#38; Mallik, K. (2023). Monitoring algorithmic fairness. In <i>Computer Aided Verification</i> (Vol. 13965, pp. 358–382). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">https://doi.org/10.1007/978-3-031-37703-7_17</a>","ama":"Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness. In: <i>Computer Aided Verification</i>. Vol 13965. Springer Nature; 2023:358–382. doi:<a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">10.1007/978-3-031-37703-7_17</a>","chicago":"Henzinger, Thomas A, Mahyar Karimi, Konstantin Kueffner, and Kaushik Mallik. “Monitoring Algorithmic Fairness.” In <i>Computer Aided Verification</i>, 13965:358–382. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">https://doi.org/10.1007/978-3-031-37703-7_17</a>.","ieee":"T. A. Henzinger, M. Karimi, K. Kueffner, and K. Mallik, “Monitoring algorithmic fairness,” in <i>Computer Aided Verification</i>, Paris, France, 2023, vol. 13965, pp. 358–382.","mla":"Henzinger, Thomas A., et al. “Monitoring Algorithmic Fairness.” <i>Computer Aided Verification</i>, vol. 13965, Springer Nature, 2023, pp. 358–382, doi:<a href=\"https://doi.org/10.1007/978-3-031-37703-7_17\">10.1007/978-3-031-37703-7_17</a>.","short":"T.A. Henzinger, M. Karimi, K. Kueffner, K. Mallik, in:, Computer Aided Verification, Springer Nature, 2023, pp. 358–382.","ista":"Henzinger TA, Karimi M, Kueffner K, Mallik K. 2023. Monitoring algorithmic fairness. Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13965, 358–382."},"date_updated":"2023-09-05T15:14:00Z","external_id":{"arxiv":["2305.15979"]},"day":"18","doi":"10.1007/978-3-031-37703-7_17","arxiv":1,"abstract":[{"lang":"eng","text":"Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. Our monitors are of two types, and use, respectively, frequentist and Bayesian statistical inference techniques. While the frequentist monitors compute estimates that are objectively correct with respect to the ground truth, the Bayesian monitors compute estimates that are correct subject to a given prior belief about the system’s model. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. Although they exhibit different theoretical complexities in certain cases, in our experiments, both frequentist and Bayesian monitors took less than a millisecond to update their verdicts after each observation."}]},{"date_updated":"2023-09-06T08:27:33Z","year":"2023","citation":{"ama":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies in LTL synthesis by semantic learning. In: <i>35th International Conference on Computer Aided Verification </i>. Vol 13964. Springer Nature; 2023:390-414. doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">10.1007/978-3-031-37706-8_20</a>","apa":"Kretinsky, J., Meggendorfer, T., Prokop, M., &#38; Rieder, S. (2023). Guessing winning policies in LTL synthesis by semantic learning. In <i>35th International Conference on Computer Aided Verification </i> (Vol. 13964, pp. 390–414). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">https://doi.org/10.1007/978-3-031-37706-8_20</a>","ieee":"J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning policies in LTL synthesis by semantic learning,” in <i>35th International Conference on Computer Aided Verification </i>, Paris, France, 2023, vol. 13964, pp. 390–414.","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In <i>35th International Conference on Computer Aided Verification </i>, 13964:390–414. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">https://doi.org/10.1007/978-3-031-37706-8_20</a>.","mla":"Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” <i>35th International Conference on Computer Aided Verification </i>, vol. 13964, Springer Nature, 2023, pp. 390–414, doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_20\">10.1007/978-3-031-37706-8_20</a>.","short":"J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 390–414.","ista":"Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies in LTL synthesis by semantic learning. 35th International Conference on Computer Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414."},"abstract":[{"text":"We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game’s huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn contrast to previous works, we (i) reflect the highly structured logical information in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii) learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning.","lang":"eng"}],"doi":"10.1007/978-3-031-37706-8_20","day":"17","ddc":["000"],"acknowledgement":"This research was funded in part by the German Research Foundation (DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).","volume":13964,"author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer"},{"full_name":"Prokop, Maximilian","first_name":"Maximilian","last_name":"Prokop"},{"last_name":"Rieder","first_name":"Sabine","full_name":"Rieder, Sabine"}],"_id":"14259","scopus_import":"1","alternative_title":["LNCS"],"title":"Guessing winning policies in LTL synthesis by semantic learning","intvolume":"     13964","publication_status":"published","department":[{"_id":"KrCh"}],"article_processing_charge":"Yes (in subscription journal)","date_created":"2023-09-03T22:01:16Z","file_date_updated":"2023-09-06T08:25:50Z","page":"390-414","quality_controlled":"1","publisher":"Springer Nature","date_published":"2023-07-17T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031377051"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"creator":"dernst","file_id":"14276","relation":"main_file","access_level":"open_access","success":1,"content_type":"application/pdf","file_name":"2023_LNCS_CAV_Kretinsky.pdf","date_updated":"2023-09-06T08:25:50Z","checksum":"ed66278b61bb869e1baba3d9b9081271","file_size":428354,"date_created":"2023-09-06T08:25:50Z"}],"publication":"35th International Conference on Computer Aided Verification ","has_accepted_license":"1","month":"07","oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"start_date":"2023-07-17","name":"CAV: Computer Aided Verification","location":"Paris, France","end_date":"2023-07-22"}},{"language":[{"iso":"eng"}],"conference":{"end_date":"2023-07-22","location":"Paris, France","name":"CAV: Computer Aided Verification","start_date":"2023-07-17"},"publication":"35th International Conference on Computer Aided Verification ","has_accepted_license":"1","month":"07","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","related_material":{"record":[{"status":"public","relation":"research_data","id":"14995"}]},"file":[{"file_name":"2023_LNCS_Koval.pdf","content_type":"application/pdf","date_updated":"2023-09-06T08:16:25Z","file_size":421408,"checksum":"c346016393123a0a2338ad4d976f61bc","date_created":"2023-09-06T08:16:25Z","creator":"dernst","file_id":"14275","access_level":"open_access","success":1,"relation":"main_file"}],"date_published":"2023-07-17T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["9783031377051"],"issn":["0302-9743"],"eissn":["1611-3349"]},"file_date_updated":"2023-09-06T08:16:25Z","page":"156-169","quality_controlled":"1","publisher":"Springer Nature","author":[{"full_name":"Koval, Nikita","last_name":"Koval","first_name":"Nikita","id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Fedorov","first_name":"Alexander","full_name":"Fedorov, Alexander","id":"2e711909-896a-11ed-bdf8-eb0f5a2984c6"},{"first_name":"Maria","last_name":"Sokolova","full_name":"Sokolova, Maria"},{"first_name":"Dmitry","last_name":"Tsitelov","full_name":"Tsitelov, Dmitry"},{"first_name":"Dan-Adrian","last_name":"Alistarh","orcid":"0000-0003-3650-940X","full_name":"Alistarh, Dan-Adrian","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87"}],"_id":"14260","scopus_import":"1","alternative_title":["LNCS"],"title":"Lincheck: A practical framework for testing concurrent data structures on JVM","intvolume":"     13964","publication_status":"published","article_processing_charge":"Yes (in subscription journal)","department":[{"_id":"DaAl"},{"_id":"GradSch"}],"date_created":"2023-09-03T22:01:16Z","ddc":["000"],"volume":13964,"date_updated":"2024-02-27T07:46:52Z","year":"2023","citation":{"ieee":"N. Koval, A. Fedorov, M. Sokolova, D. Tsitelov, and D.-A. Alistarh, “Lincheck: A practical framework for testing concurrent data structures on JVM,” in <i>35th International Conference on Computer Aided Verification </i>, Paris, France, 2023, vol. 13964, pp. 156–169.","chicago":"Koval, Nikita, Alexander Fedorov, Maria Sokolova, Dmitry Tsitelov, and Dan-Adrian Alistarh. “Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM.” In <i>35th International Conference on Computer Aided Verification </i>, 13964:156–69. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_8\">https://doi.org/10.1007/978-3-031-37706-8_8</a>.","ama":"Koval N, Fedorov A, Sokolova M, Tsitelov D, Alistarh D-A. Lincheck: A practical framework for testing concurrent data structures on JVM. In: <i>35th International Conference on Computer Aided Verification </i>. Vol 13964. Springer Nature; 2023:156-169. doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_8\">10.1007/978-3-031-37706-8_8</a>","apa":"Koval, N., Fedorov, A., Sokolova, M., Tsitelov, D., &#38; Alistarh, D.-A. (2023). Lincheck: A practical framework for testing concurrent data structures on JVM. In <i>35th International Conference on Computer Aided Verification </i> (Vol. 13964, pp. 156–169). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37706-8_8\">https://doi.org/10.1007/978-3-031-37706-8_8</a>","ista":"Koval N, Fedorov A, Sokolova M, Tsitelov D, Alistarh D-A. 2023. Lincheck: A practical framework for testing concurrent data structures on JVM. 35th International Conference on Computer Aided Verification . CAV: Computer Aided Verification, LNCS, vol. 13964, 156–169.","mla":"Koval, Nikita, et al. “Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM.” <i>35th International Conference on Computer Aided Verification </i>, vol. 13964, Springer Nature, 2023, pp. 156–69, doi:<a href=\"https://doi.org/10.1007/978-3-031-37706-8_8\">10.1007/978-3-031-37706-8_8</a>.","short":"N. Koval, A. Fedorov, M. Sokolova, D. Tsitelov, D.-A. Alistarh, in:, 35th International Conference on Computer Aided Verification , Springer Nature, 2023, pp. 156–169."},"abstract":[{"text":"This paper presents Lincheck, a new practical and user-friendly framework for testing concurrent algorithms on the Java Virtual Machine (JVM). Lincheck provides a simple and declarative way to write concurrent tests: instead of describing how to perform the test, users specify what to test by declaring all the operations to examine; the framework automatically handles the rest. As a result, tests written with Lincheck are concise and easy to understand. The framework automatically generates a set of concurrent scenarios, examines them using stress-testing or bounded model checking, and verifies that the results of each invocation are correct. Notably, if an error is detected via model checking, Lincheck provides an easy-to-follow trace to reproduce it, significantly simplifying the bug investigation.\r\n\r\nTo the best of our knowledge, Lincheck is the first production-ready tool on the JVM that offers such a simple way of writing concurrent tests, without requiring special skills or expertise. We successfully integrated Lincheck in the development process of several large projects, such as Kotlin Coroutines, and identified new bugs in popular concurrency libraries, such as a race in Java’s standard ConcurrentLinkedDeque and a liveliness bug in Java’s AbstractQueuedSynchronizer framework, which is used in most of the synchronization primitives. We believe that Lincheck can significantly improve the quality and productivity of concurrent algorithms research and development and become the state-of-the-art tool for checking their correctness.","lang":"eng"}],"doi":"10.1007/978-3-031-37706-8_8","day":"17"},{"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"oa_version":"Published Version","month":"04","has_accepted_license":"1","publication":"26th International Conference Foundations of Software Science and Computation Structures","conference":{"end_date":"2023-04-27","location":"Paris, France","name":"FOSSACS: Foundations of Software Science and Computation Structures","start_date":"2023-04-22"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308284"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2023-04-21T00:00:00Z","file":[{"checksum":"981025aed580b6b27c426cb8856cf63e","file_size":449027,"date_created":"2023-01-31T07:22:21Z","file_name":"qsl.pdf","content_type":"application/pdf","date_updated":"2023-01-31T07:22:21Z","success":1,"access_level":"open_access","relation":"main_file","creator":"esarac","file_id":"12468"},{"creator":"dernst","file_id":"13153","success":1,"relation":"main_file","access_level":"open_access","file_name":"2023_LNCS_HenzingerT.pdf","content_type":"application/pdf","date_updated":"2023-06-19T10:28:09Z","file_size":1048171,"checksum":"f16e2af1e0eb243158ab0f0fe74e7d5a","date_created":"2023-06-19T10:28:09Z"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","status":"public","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2023-01-31T07:23:56Z","publication_status":"published","intvolume":"     13992","title":"Quantitative safety and liveness","alternative_title":["LNCS"],"scopus_import":"1","_id":"12467","author":[{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"b26baa86-3308-11ec-87b0-8990f34baa85","full_name":"Mazzocchi, Nicolas Adrien","first_name":"Nicolas Adrien","last_name":"Mazzocchi"},{"full_name":"Sarac, Naci E","last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"publisher":"Springer Nature","quality_controlled":"1","ec_funded":1,"page":"349-370","file_date_updated":"2023-06-19T10:28:09Z","day":"21","doi":"10.1007/978-3-031-30829-1_17","arxiv":1,"abstract":[{"text":"Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In quantitative specification and verification, properties assign not truth values, but quantitative values to infinite traces (e.g., a cost, or the distance to a boolean property). We introduce quantitative safety and liveness, and we prove that our definitions induce conservative quantitative generalizations of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness decomposition of boolean properties. In particular, we show that every quantitative property can be written as the pointwise minimum of a quantitative safety property and a quantitative liveness property. Consequently, like boolean properties, also quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover, quantitative properties can be approximated naturally. We prove that every quantitative property that has both safe and co-safe approximations can be monitored arbitrarily precisely by a monitor that uses only a finite number of states.","lang":"eng"}],"citation":{"apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2023). Quantitative safety and liveness. In <i>26th International Conference Foundations of Software Science and Computation Structures</i> (Vol. 13992, pp. 349–370). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">https://doi.org/10.1007/978-3-031-30829-1_17</a>","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: <i>26th International Conference Foundations of Software Science and Computation Structures</i>. Vol 13992. Springer Nature; 2023:349-370. doi:<a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">10.1007/978-3-031-30829-1_17</a>","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Safety and Liveness.” In <i>26th International Conference Foundations of Software Science and Computation Structures</i>, 13992:349–70. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">https://doi.org/10.1007/978-3-031-30829-1_17</a>.","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Quantitative safety and liveness,” in <i>26th International Conference Foundations of Software Science and Computation Structures</i>, Paris, France, 2023, vol. 13992, pp. 349–370.","mla":"Henzinger, Thomas A., et al. “Quantitative Safety and Liveness.” <i>26th International Conference Foundations of Software Science and Computation Structures</i>, vol. 13992, Springer Nature, 2023, pp. 349–70, doi:<a href=\"https://doi.org/10.1007/978-3-031-30829-1_17\">10.1007/978-3-031-30829-1_17</a>.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 26th International Conference Foundations of Software Science and Computation Structures, Springer Nature, 2023, pp. 349–370.","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2023. Quantitative safety and liveness. 26th International Conference Foundations of Software Science and Computation Structures. FOSSACS: Foundations of Software Science and Computation Structures, LNCS, vol. 13992, 349–370."},"year":"2023","date_updated":"2023-07-14T11:20:27Z","external_id":{"arxiv":["2301.11175"]},"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","volume":13992,"ddc":["000"]},{"citation":{"ista":"Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 535–540.","short":"M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540.","mla":"Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>.","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 13994:535–40. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>.","ieee":"M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Paris, France, 2023, vol. 13994, pp. 535–540.","ama":"Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13994. Springer Nature; 2023:535-540. doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>","apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>"},"year":"2023","date_updated":"2023-04-25T07:02:43Z","abstract":[{"text":"The main idea behind BUBAAK is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.\r\nAt SV-COMP  2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why BUBAAK only ran several analyses in parallel, without any coordination. Still, BUBAAK won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.","lang":"eng"}],"day":"20","doi":"10.1007/978-3-031-30820-8_32","ddc":["000"],"volume":13994,"acknowledgement":"This work was supported by the ERC-2020-AdG 10102009 grant.","author":[{"first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A"}],"_id":"12854","intvolume":"     13994","alternative_title":["LNCS"],"title":"Bubaak: Runtime monitoring of program verifiers","date_created":"2023-04-20T08:22:53Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","file_date_updated":"2023-04-25T06:58:36Z","ec_funded":1,"quality_controlled":"1","page":"535-540","publisher":"Springer Nature","type":"conference","date_published":"2023-04-20T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"isbn":["9783031308192"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031308208"]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"relation":"main_file","access_level":"open_access","success":1,"creator":"dernst","file_id":"12864","file_size":16096413,"checksum":"120d2c2a38384058ad0630fdf8288312","date_created":"2023-04-25T06:58:36Z","content_type":"application/pdf","file_name":"2023_LNCS_Chalupa.pdf","date_updated":"2023-04-25T06:58:36Z"}],"has_accepted_license":"1","publication":"Tools and Algorithms for the Construction and Analysis of Systems","month":"04","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"start_date":"2023-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2023-04-27","location":"Paris, France"}},{"date_updated":"2023-04-25T07:19:07Z","year":"2023","citation":{"short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281.","mla":"Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13991, Springer Nature, 2023, pp. 260–81, doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>.","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware for best-effort third-party monitoring. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2023). Vamos: Middleware for best-effort third-party monitoring. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13991, pp. 260–281). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort third-party monitoring. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13991. Springer Nature; 2023:260-281. doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” In <i>Fundamental Approaches to Software Engineering</i>, 13991:260–81. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>.","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware for best-effort third-party monitoring,” in <i>Fundamental Approaches to Software Engineering</i>, Paris, France, 2023, vol. 13991, pp. 260–281."},"abstract":[{"lang":"eng","text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch."}],"doi":"10.1007/978-3-031-30826-0_15","day":"20","ddc":["000"],"volume":13991,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions.","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","first_name":"Marek","full_name":"Chalupa, Marek"},{"first_name":"Fabian","last_name":"Mühlböck","orcid":"0000-0003-1548-0177","full_name":"Mühlböck, Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","full_name":"Muroya Lei, Stefanie","first_name":"Stefanie","last_name":"Muroya Lei"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"}],"_id":"12856","title":"Vamos: Middleware for best-effort third-party monitoring","alternative_title":["LNCS"],"intvolume":"     13991","publication_status":"published","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2023-04-20T08:29:42Z","file_date_updated":"2023-04-25T07:16:36Z","page":"260-281","ec_funded":1,"quality_controlled":"1","publisher":"Springer Nature","date_published":"2023-04-20T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"eisbn":["9783031308260"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308253"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"12407"}]},"status":"public","file":[{"creator":"dernst","file_id":"12865","success":1,"access_level":"open_access","relation":"main_file","file_name":"2023_LNCS_ChalupaM.pdf","content_type":"application/pdf","date_updated":"2023-04-25T07:16:36Z","file_size":580828,"checksum":"17a7c8e08be609cf2408d37ea55e322c","date_created":"2023-04-25T07:16:36Z"}],"publication":"Fundamental Approaches to Software Engineering","has_accepted_license":"1","month":"04","oa_version":"Published Version","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"language":[{"iso":"eng"}],"conference":{"location":"Paris, France","end_date":"2023-04-27","name":"FASE: Fundamental Approaches to Software Engineering","start_date":"2023-04-22"}},{"date_updated":"2023-08-03T06:11:55Z","year":"2022","citation":{"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>","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>","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>.","ieee":"T. A. Henzinger, “Quantitative monitoring of software,” in <i>Software Verification</i>, New Haven, CT, United States, 2022, vol. 13124, pp. 3–6.","short":"T.A. Henzinger, in:, Software Verification, Springer Nature, 2022, 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."},"isi":1,"external_id":{"isi":["000771713200001"]},"doi":"10.1007/978-3-030-95561-8_1","day":"22","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"}],"volume":13124,"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.","_id":"10891","scopus_import":"1","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"}],"publication_status":"published","date_created":"2022-03-20T23:01:40Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","title":"Quantitative monitoring of software","intvolume":"     13124","page":"3-6","series_title":"LNCS","quality_controlled":"1","publisher":"Springer Nature","date_published":"2022-02-22T00:00:00Z","type":"conference","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783030955601"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","publication":"Software Verification","oa_version":"None","project":[{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"month":"02","language":[{"iso":"eng"}],"conference":{"location":"New Haven, CT, United States","end_date":"2021-10-19","name":"NSV: Numerical Software Verification","start_date":"2021-10-18"}},{"scopus_import":"1","_id":"11185","author":[{"full_name":"Arroyo Guevara, Alan M","orcid":"0000-0003-2401-8670","last_name":"Arroyo Guevara","first_name":"Alan M","id":"3207FDC6-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Felsner","first_name":"Stefan","full_name":"Felsner, Stefan"}],"article_processing_charge":"No","department":[{"_id":"UlWa"}],"date_created":"2022-04-17T22:01:47Z","publication_status":"published","intvolume":"     13174","title":"Approximating the bundled crossing number","ec_funded":1,"series_title":"LNCS","quality_controlled":"1","page":"383-395","publisher":"Springer Nature","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.","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>","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.","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>."},"date_updated":"2023-09-25T10:56:10Z","external_id":{"arxiv":["2109.14892"]},"day":"16","arxiv":1,"doi":"10.1007/978-3-030-96731-4_31","abstract":[{"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.","lang":"eng"}],"volume":13174,"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.","publication":"WALCOM 2022: Algorithms and Computation","project":[{"grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"oa_version":"Preprint","month":"03","language":[{"iso":"eng"}],"conference":{"name":"WALCOM: Algorithms and Computation","start_date":"2022-03-24","location":"Jember, Indonesia","end_date":"2022-03-26"},"type":"conference","date_published":"2022-03-16T00:00:00Z","publication_identifier":{"isbn":["9783030967307"],"issn":["0302-9743"],"eissn":["1611-3349"]},"oa":1,"main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.2109.14892"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","related_material":{"record":[{"status":"public","relation":"later_version","id":"13969"}]}},{"has_accepted_license":"1","publication":"Fundamental Approaches to Software Engineering","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"oa_version":"Published Version","month":"03","language":[{"iso":"eng"}],"conference":{"start_date":"2022-04-02","name":"FASE: Fundamental Approaches to Software Engineering","location":"Munich, Germany","end_date":"2022-04-07"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2022-03-29T00:00:00Z","publication_identifier":{"isbn":["9783030994280"],"issn":["0302-9743"],"eissn":["1611-3349"]},"oa":1,"file":[{"date_created":"2022-05-09T06:52:44Z","file_size":479146,"checksum":"7f6f860b20b8de2a249e9c1b4eee15cf","date_updated":"2022-05-09T06:52:44Z","content_type":"application/pdf","file_name":"2022_LNCS_Bartocci.pdf","success":1,"access_level":"open_access","relation":"main_file","file_id":"11357","creator":"dernst"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","scopus_import":"1","_id":"11355","author":[{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"last_name":"Ferrere","first_name":"Thomas","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan"},{"last_name":"Da Costa","first_name":"Ana Oliveira","full_name":"Da Costa, Ana Oliveira"}],"date_created":"2022-05-08T22:01:44Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","intvolume":"     13241","alternative_title":["LNCS"],"title":"Information-flow interfaces","ec_funded":1,"quality_controlled":"1","page":"3-22","file_date_updated":"2022-05-09T06:52:44Z","publisher":"Springer Nature","citation":{"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>.","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>","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","date_updated":"2023-08-03T07:03:40Z","external_id":{"isi":["000782393600001"]},"isi":1,"day":"29","doi":"10.1007/978-3-030-99429-7_1","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."}],"volume":13241,"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.","ddc":["000"]},{"_id":"11429","intvolume":"     13238","month":"05","alternative_title":["LNCS"],"title":"Web and Wireless Geographical Information Systems","article_processing_charge":"No","date_created":"2022-06-02T05:40:53Z","department":[{"_id":"HeEd"}],"publication_status":"published","oa_version":"None","language":[{"iso":"eng"}],"quality_controlled":"1","page":"153","editor":[{"orcid":"0000-0001-6746-4174","full_name":"Karimipour, Farid","first_name":"Farid","last_name":"Karimipour","id":"2A2BCDC4-CF62-11E9-BE5E-3B1EE6697425"},{"first_name":"Sabine","last_name":"Storandt","full_name":"Storandt, Sabine"}],"publisher":"Springer Nature","type":"book_editor","date_published":"2022-05-01T00:00:00Z","year":"2022","citation":{"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>.","short":"F. Karimipour, S. Storandt, eds., Web and Wireless Geographical Information Systems, 1st ed., Springer Nature, Cham, 2022.","ista":"Karimipour F, Storandt S eds. 2022. Web and Wireless Geographical Information Systems 1st ed., Cham: Springer Nature, 153p.","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>","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>","ieee":"F. Karimipour and S. Storandt, Eds., <i>Web and Wireless Geographical Information Systems</i>, 1st ed., vol. 13238. Cham: Springer Nature, 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>."},"date_updated":"2022-06-02T05:56:22Z","abstract":[{"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.","lang":"eng"}],"day":"01","edition":"1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031062452"],"isbn":["9783031062445"]},"doi":"10.1007/978-3-031-06245-2","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","place":"Cham","volume":13238},{"doi":"10.1007/978-3-031-07085-3_28","day":"25","abstract":[{"lang":"eng","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."}],"date_updated":"2023-08-03T07:25:02Z","year":"2022","citation":{"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>","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>","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.","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>.","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: Annual International Conference on the Theory and Applications of Cryptology and Information Security, LNCS, vol. 13276, 815–844."},"isi":1,"external_id":{"isi":["000832305300028"]},"volume":13276,"acknowledgement":"We thank Marta Mularczyk and Yiannis Tselekounis for their very helpful feedback on an earlier draft of this paper.","publication_status":"published","date_created":"2022-06-30T16:48:00Z","department":[{"_id":"GradSch"},{"_id":"KrPi"}],"article_processing_charge":"No","title":"CoCoA: Concurrent continuous group key agreement","alternative_title":["LNCS"],"intvolume":"     13276","_id":"11476","scopus_import":"1","author":[{"full_name":"Alwen, Joël","last_name":"Alwen","first_name":"Joël"},{"first_name":"Benedikt","last_name":"Auerbach","orcid":"0000-0002-7553-6606","full_name":"Auerbach, Benedikt","id":"D33D2B18-E445-11E9-ABB7-15F4E5697425"},{"id":"ffc563a3-f6e0-11ea-865d-e3cce03d17cc","last_name":"Cueto Noval","first_name":"Miguel","full_name":"Cueto Noval, Miguel"},{"id":"3E83A2F8-F248-11E8-B48F-1D18A9856A87","first_name":"Karen","last_name":"Klein","full_name":"Klein, Karen"},{"full_name":"Pascual Perez, Guillermo","last_name":"Pascual Perez","first_name":"Guillermo","id":"2D7ABD02-F248-11E8-B48F-1D18A9856A87"},{"id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","first_name":"Krzysztof Z","last_name":"Pietrzak","orcid":"0000-0002-9139-1654","full_name":"Pietrzak, Krzysztof Z"},{"first_name":"Michael","last_name":"Walter","full_name":"Walter, Michael"}],"publisher":"Springer Nature","page":"815–844","quality_controlled":"1","ec_funded":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031070853"],"isbn":["9783031070846"]},"oa":1,"date_published":"2022-05-25T00:00:00Z","type":"conference","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2022/251"}],"place":"Cham","status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa_version":"Preprint","project":[{"grant_number":"682815","name":"Teaching Old Crypto New Tricks","call_identifier":"H2020","_id":"258AA5B2-B435-11E9-9278-68D0E5697425"},{"grant_number":"665385","name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"month":"05","publication":"Advances in Cryptology – EUROCRYPT 2022","conference":{"name":"EUROCRYPT: Annual International Conference on the Theory and Applications of Cryptology and Information Security","start_date":"2022-05-30","end_date":"2022-06-03","location":"Trondheim, Norway"},"language":[{"iso":"eng"}]},{"volume":13298,"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.","external_id":{"isi":["000876977400001"],"arxiv":["2102.08703"]},"isi":1,"year":"2022","citation":{"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>.","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.","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>","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.","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.","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>."},"date_updated":"2023-08-03T12:16:29Z","abstract":[{"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.","lang":"eng"}],"day":"25","arxiv":1,"doi":"10.1007/978-3-031-09993-9_1","quality_controlled":"1","series_title":"LNCS","ec_funded":1,"page":"1-20","editor":[{"full_name":"Parter, Merav","last_name":"Parter","first_name":"Merav"}],"publisher":"Springer Nature","author":[{"last_name":"Balliu","first_name":"Alkida","full_name":"Balliu, Alkida"},{"full_name":"Hirvonen, Juho","first_name":"Juho","last_name":"Hirvonen"},{"first_name":"Darya","last_name":"Melnyk","full_name":"Melnyk, Darya"},{"last_name":"Olivetti","first_name":"Dennis","full_name":"Olivetti, Dennis"},{"last_name":"Rybicki","first_name":"Joel","full_name":"Rybicki, Joel","orcid":"0000-0002-6432-6646","id":"334EFD2E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Suomela, Jukka","first_name":"Jukka","last_name":"Suomela"}],"scopus_import":"1","_id":"11707","intvolume":"     13298","title":"Local mending","article_processing_charge":"No","department":[{"_id":"DaAl"}],"date_created":"2022-07-31T22:01:49Z","publication_status":"published","status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2102.08703"}],"type":"conference","date_published":"2022-06-25T00:00:00Z","oa":1,"publication_identifier":{"isbn":["9783031099922"],"eissn":["1611-3349"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"conference":{"end_date":"2022-06-29","location":"Paderborn, Germany","start_date":"2022-06-27","name":"SIROCCO: Structural Information and Communication Complexity"},"publication":"International Colloquium on Structural Information and Communication Complexity","month":"06","project":[{"grant_number":"840605","name":"Coordination in constrained and natural distributed systems","_id":"26A5D39A-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"oa_version":"Preprint"},{"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. "}],"day":"23","doi":"10.1007/978-3-031-17196-3_11","external_id":{"isi":["000866539700011"]},"isi":1,"citation":{"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.","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>.","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.","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>"},"year":"2022","date_updated":"2023-08-03T13:38:46Z","ddc":["000"],"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported in part by the ERC-2020-AdG 101020093.","volume":13498,"intvolume":"     13498","alternative_title":["LNCS"],"title":"Abstract monitors for quantitative specifications","article_processing_charge":"Yes","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"date_created":"2022-08-08T17:09:09Z","publication_status":"published","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Mazzocchi","first_name":"Nicolas Adrien","full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"last_name":"Sarac","first_name":"Naci E","full_name":"Sarac, Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"scopus_import":"1","_id":"11775","publisher":"Springer Nature","file_date_updated":"2023-01-20T07:34:50Z","quality_controlled":"1","ec_funded":1,"page":"200-220","oa":1,"publication_identifier":{"issn":["0302-9743"]},"type":"conference","date_published":"2022-09-23T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"creator":"dernst","file_id":"12317","success":1,"relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2022_LNCS_RV_Henzinger.pdf","date_updated":"2023-01-20T07:34:50Z","checksum":"05c7dcfbb9053a98f46441fb2eccb213","file_size":477110,"date_created":"2023-01-20T07:34:50Z"}],"month":"09","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"22nd International Conference on Runtime Verification","conference":{"name":"RV: Runtime Verification","start_date":"2022-09-28","location":"Tbilisi, Georgia","end_date":"2022-09-30"},"language":[{"iso":"eng"}]},{"file_date_updated":"2022-08-29T09:17:01Z","page":"55-78","ec_funded":1,"quality_controlled":"1","publisher":"Springer","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer"},{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"_id":"12000","scopus_import":"1","alternative_title":["LNCS"],"title":"Sound and complete certificates for auantitative termination analysis of probabilistic programs","intvolume":"     13371","publication_status":"published","article_processing_charge":"Yes (in subscription journal)","date_created":"2022-08-28T22:02:02Z","department":[{"_id":"KrCh"}],"ddc":["000"],"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.","volume":13371,"isi":1,"external_id":{"isi":["000870304500004"]},"date_updated":"2025-07-14T09:09:58Z","citation":{"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>.","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.","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.","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>.","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>"},"year":"2022","abstract":[{"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.","lang":"eng"}],"doi":"10.1007/978-3-031-13185-1_4","day":"07","language":[{"iso":"eng"}],"conference":{"location":"Haifa, Israel","end_date":"2022-08-10","name":"CAV: Computer Aided Verification","start_date":"2022-08-07"},"publication":"Proceedings of the 34th International Conference on Computer Aided Verification","has_accepted_license":"1","month":"08","oa_version":"Published Version","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"14539"}]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","file":[{"date_created":"2022-08-29T09:17:01Z","file_size":505094,"checksum":"24e0f810ec52735a90ade95198bc641d","date_updated":"2022-08-29T09:17:01Z","content_type":"application/pdf","file_name":"2022_LNCS_Chatterjee.pdf","access_level":"open_access","success":1,"relation":"main_file","file_id":"12003","creator":"alisjak"}],"date_published":"2022-08-07T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031131844"]}},{"conference":{"start_date":"2022-05-02","name":"FC: Financial Cryptography and Data Security","location":"Grenada","end_date":"2022-05-06"},"language":[{"iso":"eng"}],"oa_version":"Preprint","month":"10","publication":"Financial Cryptography and Data Security","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2110.08848"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publication_identifier":{"isbn":["9783031182822"],"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031182839"]},"oa":1,"type":"conference","date_published":"2022-10-22T00:00:00Z","publisher":"Springer Nature","quality_controlled":"1","page":"358-373","department":[{"_id":"KrPi"}],"date_created":"2023-01-12T12:10:38Z","article_processing_charge":"No","publication_status":"published","intvolume":"     13411","alternative_title":["LNCS"],"title":"Hide & Seek: Privacy-preserving rebalancing on payment channel networks","scopus_import":"1","_id":"12167","author":[{"full_name":"Avarikioti, Georgia","first_name":"Georgia","last_name":"Avarikioti","id":"c20482a0-3b89-11eb-9862-88cf6404b88c"},{"id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9139-1654","full_name":"Pietrzak, Krzysztof Z","first_name":"Krzysztof Z","last_name":"Pietrzak"},{"full_name":"Salem, Iosif","first_name":"Iosif","last_name":"Salem"},{"full_name":"Schmid, Stefan","last_name":"Schmid","first_name":"Stefan"},{"last_name":"Tiwari","first_name":"Samarth","full_name":"Tiwari, Samarth"},{"id":"2D82B818-F248-11E8-B48F-1D18A9856A87","last_name":"Yeo","first_name":"Michelle X","full_name":"Yeo, Michelle X"}],"volume":13411,"day":"22","doi":"10.1007/978-3-031-18283-9_17","arxiv":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."}],"citation":{"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>.","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.","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>","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."},"year":"2022","date_updated":"2023-09-05T15:10:57Z","external_id":{"arxiv":["2110.08848"]}},{"external_id":{"arxiv":["2110.00960"]},"date_updated":"2023-09-05T15:11:35Z","year":"2022","citation":{"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.","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>.","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>.","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>"},"abstract":[{"lang":"eng","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."}],"arxiv":1,"doi":"10.1007/978-3-031-18283-9_13","day":"22","volume":13411,"author":[{"full_name":"Cohen, Shir","first_name":"Shir","last_name":"Cohen"},{"full_name":"Gelashvili, Rati","first_name":"Rati","last_name":"Gelashvili"},{"full_name":"Kokoris Kogias, Eleftherios","last_name":"Kokoris Kogias","first_name":"Eleftherios","id":"f5983044-d7ef-11ea-ac6d-fd1430a26d30"},{"first_name":"Zekun","last_name":"Li","full_name":"Li, Zekun"},{"full_name":"Malkhi, Dahlia","last_name":"Malkhi","first_name":"Dahlia"},{"full_name":"Sonnino, Alberto","last_name":"Sonnino","first_name":"Alberto"},{"first_name":"Alexander","last_name":"Spiegelman","full_name":"Spiegelman, Alexander"}],"_id":"12168","scopus_import":"1","title":"Be aware of your leaders","alternative_title":["LNCS"],"intvolume":"     13411","publication_status":"published","article_processing_charge":"No","department":[{"_id":"ElKo"}],"date_created":"2023-01-12T12:10:49Z","page":"279-295","quality_controlled":"1","publisher":"Springer Nature","date_published":"2022-10-22T00:00:00Z","type":"conference","oa":1,"publication_identifier":{"isbn":["9783031182822"],"eisbn":["9783031182839"],"issn":["0302-9743"],"eissn":["1611-3349"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2110.00960"}],"publication":"International Conference on Financial Cryptography and Data Security","month":"10","oa_version":"Preprint","language":[{"iso":"eng"}],"conference":{"location":"Grenada","end_date":"2022-05-06","name":"FC: Financial Cryptography and Data Security","start_date":"2022-05-02"}},{"language":[{"iso":"eng"}],"conference":{"end_date":"2022-10-28","location":"Virtual","name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2022-10-25"},"publication":"20th International Symposium on Automated Technology for Verification and Analysis","month":"10","oa_version":"None","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","type":"conference","date_published":"2022-10-21T00:00:00Z","publication_identifier":{"isbn":["9783031199912"],"eisbn":["9783031199929"],"issn":["0302-9743"],"eissn":["1611-3349"]},"quality_controlled":"1","page":"320-326","publisher":"Springer Nature","author":[{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer"}],"scopus_import":"1","_id":"12170","intvolume":"     13505","alternative_title":["LNCS"],"title":"PET – A partial exploration tool for probabilistic verification","department":[{"_id":"KrCh"}],"date_created":"2023-01-12T12:11:07Z","article_processing_charge":"No","publication_status":"published","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.","volume":13505,"citation":{"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.","short":"T. Meggendorfer, in:, 20th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2022, pp. 320–326.","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>.","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>.","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>","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>"},"year":"2022","date_updated":"2023-09-05T15:11:51Z","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."}],"day":"21","doi":"10.1007/978-3-031-19992-9_20"}]