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