[{"date_published":"2026-01-01T00:00:00Z","_id":"21042","intvolume":"     15751","publication_status":"published","language":[{"iso":"eng"}],"doi":"10.1007/978-3-032-07024-1_18","date_created":"2026-01-25T23:01:40Z","oa_version":"Preprint","article_processing_charge":"No","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2502.10074","open_access":"1"}],"title":"Anthemius: Efficient and modular block assembly for concurrent execution","department":[{"_id":"KrPi"}],"acknowledgement":"This work was supported by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502 and the Vienna Science and Technology Fund (WWTF) project SCALE2 CT22-045.","corr_author":"1","publication_identifier":{"isbn":["9783032070234"],"eissn":["1611-3349"],"issn":["0302-9743"]},"external_id":{"arxiv":["2502.10074"]},"project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"},{"_id":"7bdd2f70-9f16-11ee-852c-b7950bc6d277","name":"SeCure, privAte, and interoperabLe layEr 2","grant_number":"ICT22-045"}],"month":"01","arxiv":1,"type":"conference","abstract":[{"text":"Many blockchains such as Ethereum execute all incoming transactions sequentially significantly limiting the potential throughput. A common approach to scale execution is parallel execution engines that fully utilize modern multi-core architectures. Parallel execution is then either done optimistically, by executing transactions in parallel and detecting conflicts on the fly, or guided, by requiring exhaustive client transaction hints and scheduling transactions accordingly.\r\n\r\nHowever, recent studies have shown that the performance of parallel execution engines depends on the nature of the underlying workload. In fact, in some cases, only a 60% speed-up compared to sequential execution could be obtained. This is the case, as transactions that access the same resources must be executed sequentially. For example, if 10% of the transactions in a block access the same resource, the execution cannot meaningfully scale beyond 10 cores. Therefore, a single popular application can bottleneck the execution and limit the potential throughput.\r\n\r\nIn this paper, we introduce Anthemius, a block construction algorithm that optimizes parallel transaction execution throughput. We evaluate Anthemius exhaustively under a range of workloads, and show that Anthemius enables the underlying parallel execution engine to process over twice as many transactions.","lang":"eng"}],"date_updated":"2026-02-12T13:39:07Z","author":[{"id":"f09651b9-fec0-11ec-b5d8-934aff0e52a4","orcid":"0000-0001-7227-8309","full_name":"Neiheiser, Ray","last_name":"Neiheiser","first_name":"Ray"},{"id":"f5983044-d7ef-11ea-ac6d-fd1430a26d30","orcid":"0000-0002-8827-3382","last_name":"Kokoris Kogias","first_name":"Eleftherios","full_name":"Kokoris Kogias, Eleftherios"}],"year":"2026","OA_type":"green","page":"307-323","citation":{"short":"R. Neiheiser, E. Kokoris Kogias, in:, 29th International Conference on Financial Cryptography and Data Security, Springer Nature, 2026, pp. 307–323.","ista":"Neiheiser R, Kokoris Kogias E. 2026. Anthemius: Efficient and modular block assembly for concurrent execution. 29th International Conference on Financial Cryptography and Data Security. FC: Financial Cryptography and Data Security, LNCS, vol. 15751, 307–323.","chicago":"Neiheiser, Ray, and Eleftherios Kokoris Kogias. “Anthemius: Efficient and Modular Block Assembly for Concurrent Execution.” In <i>29th International Conference on Financial Cryptography and Data Security</i>, 15751:307–23. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-07024-1_18\">https://doi.org/10.1007/978-3-032-07024-1_18</a>.","ieee":"R. Neiheiser and E. Kokoris Kogias, “Anthemius: Efficient and modular block assembly for concurrent execution,” in <i>29th International Conference on Financial Cryptography and Data Security</i>, Miyakojima, Japan, 2026, vol. 15751, pp. 307–323.","mla":"Neiheiser, Ray, and Eleftherios Kokoris Kogias. “Anthemius: Efficient and Modular Block Assembly for Concurrent Execution.” <i>29th International Conference on Financial Cryptography and Data Security</i>, vol. 15751, Springer Nature, 2026, pp. 307–23, doi:<a href=\"https://doi.org/10.1007/978-3-032-07024-1_18\">10.1007/978-3-032-07024-1_18</a>.","ama":"Neiheiser R, Kokoris Kogias E. Anthemius: Efficient and modular block assembly for concurrent execution. In: <i>29th International Conference on Financial Cryptography and Data Security</i>. Vol 15751. Springer Nature; 2026:307-323. doi:<a href=\"https://doi.org/10.1007/978-3-032-07024-1_18\">10.1007/978-3-032-07024-1_18</a>","apa":"Neiheiser, R., &#38; Kokoris Kogias, E. (2026). Anthemius: Efficient and modular block assembly for concurrent execution. In <i>29th International Conference on Financial Cryptography and Data Security</i> (Vol. 15751, pp. 307–323). Miyakojima, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-07024-1_18\">https://doi.org/10.1007/978-3-032-07024-1_18</a>"},"status":"public","publication":"29th International Conference on Financial Cryptography and Data Security","conference":{"location":"Miyakojima, Japan","name":"FC: Financial Cryptography and Data Security","start_date":"2025-04-14","end_date":"2025-04-18"},"publisher":"Springer Nature","scopus_import":"1","volume":15751,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","day":"01","alternative_title":["LNCS"],"oa":1,"quality_controlled":"1"},{"oa":1,"quality_controlled":"1","volume":15751,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","alternative_title":["LNCS"],"day":"01","OA_type":"green","citation":{"ista":"Kniep Q, Kokoris Kogias E, Sonnino A, Zablotchi I, Zhang N. 2026. Pilotfish: Distributed execution for scalable blockchains. 29th International Conference on Financial Cryptography and Data Security. FC: Financial Cryptography and Data Security, LNCS, vol. 15751, 287–306.","short":"Q. Kniep, E. Kokoris Kogias, A. Sonnino, I. Zablotchi, N. Zhang, in:, 29th International Conference on Financial Cryptography and Data Security, Springer Nature, 2026, pp. 287–306.","chicago":"Kniep, Quentin, Eleftherios Kokoris Kogias, Alberto Sonnino, Igor Zablotchi, and Nuda Zhang. “Pilotfish: Distributed Execution for Scalable Blockchains.” In <i>29th International Conference on Financial Cryptography and Data Security</i>, 15751:287–306. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-07024-1_17\">https://doi.org/10.1007/978-3-032-07024-1_17</a>.","mla":"Kniep, Quentin, et al. “Pilotfish: Distributed Execution for Scalable Blockchains.” <i>29th International Conference on Financial Cryptography and Data Security</i>, vol. 15751, Springer Nature, 2026, pp. 287–306, doi:<a href=\"https://doi.org/10.1007/978-3-032-07024-1_17\">10.1007/978-3-032-07024-1_17</a>.","ama":"Kniep Q, Kokoris Kogias E, Sonnino A, Zablotchi I, Zhang N. Pilotfish: Distributed execution for scalable blockchains. In: <i>29th International Conference on Financial Cryptography and Data Security</i>. Vol 15751. Springer Nature; 2026:287-306. doi:<a href=\"https://doi.org/10.1007/978-3-032-07024-1_17\">10.1007/978-3-032-07024-1_17</a>","apa":"Kniep, Q., Kokoris Kogias, E., Sonnino, A., Zablotchi, I., &#38; Zhang, N. (2026). Pilotfish: Distributed execution for scalable blockchains. In <i>29th International Conference on Financial Cryptography and Data Security</i> (Vol. 15751, pp. 287–306). Miyakojima, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-07024-1_17\">https://doi.org/10.1007/978-3-032-07024-1_17</a>","ieee":"Q. Kniep, E. Kokoris Kogias, A. Sonnino, I. Zablotchi, and N. Zhang, “Pilotfish: Distributed execution for scalable blockchains,” in <i>29th International Conference on Financial Cryptography and Data Security</i>, Miyakojima, Japan, 2026, vol. 15751, pp. 287–306."},"page":"287-306","publication":"29th International Conference on Financial Cryptography and Data Security","status":"public","scopus_import":"1","publisher":"Springer Nature","conference":{"location":"Miyakojima, Japan","name":"FC: Financial Cryptography and Data Security","start_date":"2025-04-14","end_date":"2025-04-18"},"date_updated":"2026-02-16T07:56:09Z","year":"2026","author":[{"first_name":"Quentin","last_name":"Kniep","full_name":"Kniep, Quentin"},{"full_name":"Kokoris Kogias, Eleftherios","first_name":"Eleftherios","last_name":"Kokoris Kogias","orcid":"0000-0002-8827-3382","id":"f5983044-d7ef-11ea-ac6d-fd1430a26d30"},{"full_name":"Sonnino, Alberto","last_name":"Sonnino","first_name":"Alberto"},{"full_name":"Zablotchi, Igor","first_name":"Igor","last_name":"Zablotchi"},{"full_name":"Zhang, Nuda","first_name":"Nuda","last_name":"Zhang"}],"publication_identifier":{"isbn":["9783032070234"],"issn":["0302-9743"],"eissn":["1611-3349"]},"external_id":{"arxiv":["2401.16292"]},"abstract":[{"text":"Scalability is a crucial requirement for modern large-scale systems, enabling elasticity and ensuring responsiveness under varying load. While cloud systems have achieved scalable architectures, blockchain systems remain constrained by the need to over-provision validator machines to handle peak load. This leads to resource inefficiency, poor cost scaling, and limits on performance. To address these challenges, we introduce Pilotfish, the first scale-out transaction execution engine for blockchains. Pilotfish enables validators to scale horizontally by distributing transaction execution across multiple worker machines, allowing elasticity without compromising consistency or determinism. It integrates seamlessly with the lazy blockchain architecture, completing the missing piece of execution elasticity. To achieve this, Pilotfish tackles several key challenges: ensuring scalable and strongly consistent distributed transactions, handling partial crash recovery with lightweight replication, and maintaining concurrency with a novel versioned-queue scheduling algorithm. Our evaluation shows that Pilotfish scales linearly up to at least eight workers per validator for compute-bound workloads, while maintaining low latency. By solving scalable execution, Pilotfish brings blockchains closer to achieving end-to-end elasticity, unlocking new possibilities for efficient and adaptable blockchain systems.","lang":"eng"}],"type":"conference","month":"01","arxiv":1,"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2401.16292","open_access":"1"}],"article_processing_charge":"No","oa_version":"Preprint","doi":"10.1007/978-3-032-07024-1_17","date_created":"2026-01-25T23:01:41Z","title":"Pilotfish: Distributed execution for scalable blockchains","publication_status":"published","intvolume":"     15751","language":[{"iso":"eng"}],"date_published":"2026-01-01T00:00:00Z","_id":"21044"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","day":"03","alternative_title":["LNCS"],"volume":16318,"oa":1,"quality_controlled":"1","author":[{"first_name":"Jakob","last_name":"Troidl","full_name":"Troidl, Jakob"},{"first_name":"Yiqing","last_name":"Liang","full_name":"Liang, Yiqing"},{"last_name":"Beyer","first_name":"Johanna","full_name":"Beyer, Johanna"},{"id":"3A0A06F4-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-7667-6854","first_name":"Mojtaba","last_name":"Tavakoli","full_name":"Tavakoli, Mojtaba"},{"orcid":"0000-0001-8559-3973","id":"42EFD3B6-F248-11E8-B48F-1D18A9856A87","last_name":"Danzl","first_name":"Johann G","full_name":"Danzl, Johann G"},{"full_name":"Hadwiger, Markus","first_name":"Markus","last_name":"Hadwiger"},{"full_name":"Pfister, Hanspeter","last_name":"Pfister","first_name":"Hanspeter"},{"last_name":"Tompkin","first_name":"James","full_name":"Tompkin, James"}],"year":"2026","date_updated":"2026-02-16T08:50:50Z","conference":{"location":"Daejeon, South Korea","name":"EMA4MICCAI: Efficient Medical Artificial Intelligence","end_date":"2025-09-23","start_date":"2025-09-23"},"publisher":"Springer Nature","scopus_import":"1","page":"257-267","OA_type":"green","citation":{"ieee":"J. Troidl <i>et al.</i>, “niiv: Interactive Self-supervised Neural Implicit Isotropic Volume Reconstruction,” in <i>1st International Workshop on Efficient Medical Artificial Intelligence</i>, Daejeon, South Korea, 2026, vol. 16318, pp. 257–267.","mla":"Troidl, Jakob, et al. “Niiv: Interactive Self-Supervised Neural Implicit Isotropic Volume Reconstruction.” <i>1st International Workshop on Efficient Medical Artificial Intelligence</i>, vol. 16318, Springer Nature, 2026, pp. 257–67, doi:<a href=\"https://doi.org/10.1007/978-3-032-13961-0_26\">10.1007/978-3-032-13961-0_26</a>.","apa":"Troidl, J., Liang, Y., Beyer, J., Tavakoli, M., Danzl, J. G., Hadwiger, M., … Tompkin, J. (2026). niiv: Interactive Self-supervised Neural Implicit Isotropic Volume Reconstruction. In <i>1st International Workshop on Efficient Medical Artificial Intelligence</i> (Vol. 16318, pp. 257–267). Daejeon, South Korea: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-13961-0_26\">https://doi.org/10.1007/978-3-032-13961-0_26</a>","ama":"Troidl J, Liang Y, Beyer J, et al. niiv: Interactive Self-supervised Neural Implicit Isotropic Volume Reconstruction. In: <i>1st International Workshop on Efficient Medical Artificial Intelligence</i>. Vol 16318. Springer Nature; 2026:257-267. doi:<a href=\"https://doi.org/10.1007/978-3-032-13961-0_26\">10.1007/978-3-032-13961-0_26</a>","short":"J. Troidl, Y. Liang, J. Beyer, M. Tavakoli, J.G. Danzl, M. Hadwiger, H. Pfister, J. Tompkin, in:, 1st International Workshop on Efficient Medical Artificial Intelligence, Springer Nature, 2026, pp. 257–267.","ista":"Troidl J, Liang Y, Beyer J, Tavakoli M, Danzl JG, Hadwiger M, Pfister H, Tompkin J. 2026. niiv: Interactive Self-supervised Neural Implicit Isotropic Volume Reconstruction. 1st International Workshop on Efficient Medical Artificial Intelligence. EMA4MICCAI: Efficient Medical Artificial Intelligence, LNCS, vol. 16318, 257–267.","chicago":"Troidl, Jakob, Yiqing Liang, Johanna Beyer, Mojtaba Tavakoli, Johann G Danzl, Markus Hadwiger, Hanspeter Pfister, and James Tompkin. “Niiv: Interactive Self-Supervised Neural Implicit Isotropic Volume Reconstruction.” In <i>1st International Workshop on Efficient Medical Artificial Intelligence</i>, 16318:257–67. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-13961-0_26\">https://doi.org/10.1007/978-3-032-13961-0_26</a>."},"publication":"1st International Workshop on Efficient Medical Artificial Intelligence","status":"public","department":[{"_id":"JoDa"}],"date_created":"2026-02-01T23:01:44Z","oa_version":"Preprint","doi":"10.1007/978-3-032-13961-0_26","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1101/2024.09.07.611785"}],"title":"niiv: Interactive Self-supervised Neural Implicit Isotropic Volume Reconstruction","type":"conference","month":"01","abstract":[{"lang":"eng","text":"Three-dimensional (3D) microscopy data is often anisotropic with significantly lower resolution (up to 8x) along the z axis than along the xy axes. Computationally generating plausible isotropic resolution from anisotropic imaging data would benefit the visual analysis of large-scale volumes. This paper proposes niiv, a self-supervised method for isotropic reconstruction of 3D microscopy data that can quickly produce images at arbitrary output resolutions. The representation embeds a learned latent code within a neural field that describes the implicit higher-resolution isotropic image region. We use an attention-guided latent interpolation approach, which allows flexible information exchange over a local latent neighborhood. Under isotropic volume assumptions, we self-supervise this representation on low-/high-resolution lateral image pairs to reconstruct an isotropic volume from low-resolution axial images. We evaluate our method on simulated and real anisotropic electron (EM) and light microscopy (LM) data. Compared to diffusion-based baselines, niiv shows improved reconstruction quality (+1 dB PSNR) and is over three orders of magnitude faster (1,000x) to infer. Specifically, niiv reconstructs a 128^3 voxel volume in 2/10th of a second, renderable at varying (continuous) high resolutions for display. Our code is available at https://github.com/jakobtroidl/niiv-miccai."}],"acknowledgement":"This work was supported by NIH grants 1U01NS132158 and R01HD104969. We thank the reviewers for their constructive feedback.","publication_identifier":{"isbn":["9783032139603"],"eissn":["1611-3349"],"issn":["0302-9743"]},"_id":"21135","related_material":{"link":[{"url":"https://github.com/jakobtroidl/niiv-miccai","relation":"software"}]},"date_published":"2026-01-03T00:00:00Z","language":[{"iso":"eng"}],"intvolume":"     16318","publication_status":"published"},{"OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"13","alternative_title":["LNCS"],"volume":16448,"oa":1,"quality_controlled":"1","author":[{"full_name":"Antić, Todor","last_name":"Antić","first_name":"Todor"},{"last_name":"Džuklevski","first_name":"Aleksa","full_name":"Džuklevski, Aleksa"},{"first_name":"Jiří","last_name":"Fiala","full_name":"Fiala, Jiří"},{"first_name":"Jan","last_name":"Kratochvíl","full_name":"Kratochvíl, Jan"},{"full_name":"Liotta, Giuseppe","first_name":"Giuseppe","last_name":"Liotta"},{"id":"f86f7148-b140-11ec-9577-95435b8df824","full_name":"Saghafian, Morteza","first_name":"Morteza","last_name":"Saghafian"},{"full_name":"Saumell, Maria","last_name":"Saumell","first_name":"Maria"},{"full_name":"Zink, Johannes","first_name":"Johannes","last_name":"Zink"}],"year":"2026","date_updated":"2026-03-02T08:49:20Z","publisher":"Springer Nature","conference":{"location":"Krakow, Poland","end_date":"2026-02-13","start_date":"2026-02-09","name":"SOFSEM: Conference on Current Trends in Theory and Practice of Computer Science"},"scopus_import":"1","OA_type":"green","page":"532-546","citation":{"ama":"Antić T, Džuklevski A, Fiala J, et al. Edge-constrained Hamiltonian paths on a point set. In: <i>51st International Conference on Current Trends in Theory and Practice of Computer Science</i>. Vol 16448. Springer Nature; 2026:532-546. doi:<a href=\"https://doi.org/10.1007/978-3-032-17801-5_39\">10.1007/978-3-032-17801-5_39</a>","mla":"Antić, Todor, et al. “Edge-Constrained Hamiltonian Paths on a Point Set.” <i>51st International Conference on Current Trends in Theory and Practice of Computer Science</i>, vol. 16448, Springer Nature, 2026, pp. 532–46, doi:<a href=\"https://doi.org/10.1007/978-3-032-17801-5_39\">10.1007/978-3-032-17801-5_39</a>.","apa":"Antić, T., Džuklevski, A., Fiala, J., Kratochvíl, J., Liotta, G., Saghafian, M., … Zink, J. (2026). Edge-constrained Hamiltonian paths on a point set. In <i>51st International Conference on Current Trends in Theory and Practice of Computer Science</i> (Vol. 16448, pp. 532–546). Krakow, Poland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-17801-5_39\">https://doi.org/10.1007/978-3-032-17801-5_39</a>","ieee":"T. Antić <i>et al.</i>, “Edge-constrained Hamiltonian paths on a point set,” in <i>51st International Conference on Current Trends in Theory and Practice of Computer Science</i>, Krakow, Poland, 2026, vol. 16448, pp. 532–546.","chicago":"Antić, Todor, Aleksa Džuklevski, Jiří Fiala, Jan Kratochvíl, Giuseppe Liotta, Morteza Saghafian, Maria Saumell, and Johannes Zink. “Edge-Constrained Hamiltonian Paths on a Point Set.” In <i>51st International Conference on Current Trends in Theory and Practice of Computer Science</i>, 16448:532–46. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-17801-5_39\">https://doi.org/10.1007/978-3-032-17801-5_39</a>.","ista":"Antić T, Džuklevski A, Fiala J, Kratochvíl J, Liotta G, Saghafian M, Saumell M, Zink J. 2026. Edge-constrained Hamiltonian paths on a point set. 51st International Conference on Current Trends in Theory and Practice of Computer Science. SOFSEM: Conference on Current Trends in Theory and Practice of Computer Science, LNCS, vol. 16448, 532–546.","short":"T. Antić, A. Džuklevski, J. Fiala, J. Kratochvíl, G. Liotta, M. Saghafian, M. Saumell, J. Zink, in:, 51st International Conference on Current Trends in Theory and Practice of Computer Science, Springer Nature, 2026, pp. 532–546."},"publication":"51st International Conference on Current Trends in Theory and Practice of Computer Science","status":"public","department":[{"_id":"HeEd"}],"doi":"10.1007/978-3-032-17801-5_39","oa_version":"Preprint","date_created":"2026-03-01T23:01:40Z","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2511.22526"}],"title":"Edge-constrained Hamiltonian paths on a point set","external_id":{"arxiv":["2511.22526"]},"month":"02","arxiv":1,"type":"conference","abstract":[{"lang":"eng","text":"Let . S be a set of distinct points in general position in the\r\nEuclidean plane. A plane Hamiltonian path on . S is a crossing-free geometric path such that every point of .S is a vertex of the path. It is\r\nknown that, if. S is sufficiently large, there exist three edge-disjoint plane\r\nHamiltonian paths on . S. In this paper we study an edge-constrained\r\nversion of the problem of finding Hamiltonian paths on a point set. We\r\nfirst consider the problem of finding a single plane Hamiltonian path . π\r\nwith endpoints .s, t ∈ S and constraints given by a segment . ab, where\r\n.a, b ∈ S. We consider the following scenarios: (i) .ab ∈ π; (ii) .ab π. We\r\ncharacterize those quintuples . S, a, b, s, t for which . π exists. Secondly,\r\nwe consider the problem of finding two plane Hamiltonian paths . π1, π2\r\non a set . S with constraints given by a segment . ab, where .a, b ∈ S. We\r\nconsider the following scenarios: (i) .π1 and .π2 share no edges and .ab is\r\nan edge of . π1; (ii) .π1 and .π2 share no edges and none of them includes\r\n.ab as an edge; (iii) both .π1 and .π2 include .ab as an edge and share no\r\nother edges. In all cases, we characterize those triples . S, a, b for which\r\n.π1 and .π2 exist."}],"acknowledgement":"We thank the organizers of the HOMONOLO 2024 workshop in Nová Louka, Czech Republic, for the fruitful atmosphere where the research on this project was initiated.\r\n\r\nT. Antić, A. Džuklevski, J. Kratochvíl and M. Saumell received funding from GAČR grant 23–04949X, T.A and A.Dž were additionally supported by GAUK grant SVV–2025–260822. G. Liotta was supported in part by MUR of Italy, PRIN Project no. 2022TS4Y3N – EXPAND and PON Project ARS01_00540. J. Fiala was in part supported by GAČR grant 25-16847S.","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783032178008"]},"_id":"21374","date_published":"2026-02-13T00:00:00Z","language":[{"iso":"eng"}],"intvolume":"     16448","publication_status":"published"},{"title":"On the MST-ratio: Theoretical bounds and complexity of finding the maximum","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2409.11079","open_access":"1"}],"article_processing_charge":"No","doi":"10.1007/978-981-95-7127-7_26","oa_version":"Preprint","date_created":"2026-03-08T23:01:45Z","department":[{"_id":"HeEd"}],"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9789819571260"]},"acknowledgement":"A. J. Ameli—Supported by the project COALESCE (ERC grant no. 853234).\r\nM. Saghafian—Partially supported by the European Research Council (ERC), grant no. 788183, and by the Wittgenstein Prize, Austrian Science Fund (FWF), grant no. Z 342-N31.","abstract":[{"text":"Given a finite set of red and blue points in R^d, the MST-ratio is defined as the total length of the Euclidean minimum spanning trees of the red points and the blue points, divided by the length of the Euclidean minimum spanning tree of their union. The MST-ratio has recently gained attention due to its direct interpretation in topological models for studying point sets with applications in spatial biology. The maximum MST-ratio of a point set is the maximum MST-ratio over all proper colorings of its points by red and blue. We prove that finding the maximum MST-ratio of a given point set is NP-hard when the dimension is part of the input. Moreover, we present a quadratic-time 3-approximation algorithm for this problem. As part of the proof, we show that in any metric space, the maximum MST-ratio is smaller than 3. Furthermore, we study the average MST-ratio over all colorings of a set of n points. We show that this average is always at least n-2/n-1, and for n random points uniformly distributed in a d-dimensional unit cube, the average tends to (math formular) in expectation as n approaches infinity.","lang":"eng"}],"type":"conference","arxiv":1,"month":"02","project":[{"call_identifier":"H2020","grant_number":"788183","name":"Alpha Shape Theory Extended","_id":"266A2E9E-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z00342","name":"Mathematics, Computer Science","_id":"268116B8-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"external_id":{"arxiv":["2409.11079"]},"date_published":"2026-02-14T00:00:00Z","_id":"21410","publication_status":"published","intvolume":"     16444","language":[{"iso":"eng"}],"volume":16444,"alternative_title":["LNCS"],"day":"14","OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","oa":1,"date_updated":"2026-03-09T10:25:41Z","year":"2026","author":[{"last_name":"Jabal Ameli","first_name":"Afrouz","full_name":"Jabal Ameli, Afrouz"},{"full_name":"Motiei, Faezeh","first_name":"Faezeh","last_name":"Motiei"},{"id":"f86f7148-b140-11ec-9577-95435b8df824","first_name":"Morteza","last_name":"Saghafian","full_name":"Saghafian, Morteza"}],"status":"public","publication":"20th International Conference and Workshops on Algorithms and Computation","citation":{"ista":"Jabal Ameli A, Motiei F, Saghafian M. 2026. On the MST-ratio: Theoretical bounds and complexity of finding the maximum. 20th International Conference and Workshops on Algorithms and Computation. WALCOM: International Conference and Workshops on Algorithms and Computation, LNCS, vol. 16444, 386–401.","short":"A. Jabal Ameli, F. Motiei, M. Saghafian, in:, 20th International Conference and Workshops on Algorithms and Computation, Springer Nature, 2026, pp. 386–401.","chicago":"Jabal Ameli, Afrouz, Faezeh Motiei, and Morteza Saghafian. “On the MST-Ratio: Theoretical Bounds and Complexity of Finding the Maximum.” In <i>20th International Conference and Workshops on Algorithms and Computation</i>, 16444:386–401. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-981-95-7127-7_26\">https://doi.org/10.1007/978-981-95-7127-7_26</a>.","apa":"Jabal Ameli, A., Motiei, F., &#38; Saghafian, M. (2026). On the MST-ratio: Theoretical bounds and complexity of finding the maximum. In <i>20th International Conference and Workshops on Algorithms and Computation</i> (Vol. 16444, pp. 386–401). Perugia, Italy: Springer Nature. <a href=\"https://doi.org/10.1007/978-981-95-7127-7_26\">https://doi.org/10.1007/978-981-95-7127-7_26</a>","ama":"Jabal Ameli A, Motiei F, Saghafian M. On the MST-ratio: Theoretical bounds and complexity of finding the maximum. In: <i>20th International Conference and Workshops on Algorithms and Computation</i>. Vol 16444. Springer Nature; 2026:386-401. doi:<a href=\"https://doi.org/10.1007/978-981-95-7127-7_26\">10.1007/978-981-95-7127-7_26</a>","mla":"Jabal Ameli, Afrouz, et al. “On the MST-Ratio: Theoretical Bounds and Complexity of Finding the Maximum.” <i>20th International Conference and Workshops on Algorithms and Computation</i>, vol. 16444, Springer Nature, 2026, pp. 386–401, doi:<a href=\"https://doi.org/10.1007/978-981-95-7127-7_26\">10.1007/978-981-95-7127-7_26</a>.","ieee":"A. Jabal Ameli, F. Motiei, and M. Saghafian, “On the MST-ratio: Theoretical bounds and complexity of finding the maximum,” in <i>20th International Conference and Workshops on Algorithms and Computation</i>, Perugia, Italy, 2026, vol. 16444, pp. 386–401."},"OA_type":"green","page":"386-401","ec_funded":1,"scopus_import":"1","conference":{"location":"Perugia, Italy","start_date":"2026-03-04","end_date":"2026-03-06","name":"WALCOM: International Conference and Workshops on Algorithms and Computation"},"publisher":"Springer Nature"},{"date_published":"2026-01-01T00:00:00Z","_id":"21134","related_material":{"record":[{"id":"21651","relation":"dissertation_contains","status":"public"}]},"publication_status":"published","intvolume":"     15752","language":[{"iso":"eng"}],"title":"On the (in)security of Proofs-of-space based longest-chain blockchains","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2505.14891","open_access":"1"}],"article_processing_charge":"No","date_created":"2026-02-01T23:01:43Z","doi":"10.1007/978-3-032-07035-7_8","oa_version":"Preprint","department":[{"_id":"KrPi"}],"publication_identifier":{"isbn":["9783032070340"],"eissn":["1611-3349"],"issn":["0302-9743"]},"corr_author":"1","acknowledgement":"This research was funded in whole or in part by the Austrian Science Fund (FWF) 10.55776/F85.","abstract":[{"lang":"eng","text":"The Nakamoto consensus protocol underlying the Bitcoin blockchain uses proof of work as a voting mechanism. Honest miners who contribute hashing power towards securing the chain try to extend the longest chain they are aware of. Despite its simplicity, Nakamoto consensus achieves meaningful security guarantees assuming that at any point in time, a majority of the hashing power is controlled by honest parties. This also holds under “resource variability”, i.e., if the total hashing power varies greatly over time.\r\nProofs of space (PoSpace) have been suggested as a more sustainable replacement for proofs of work. Unfortunately, no construction of a “longest-chain” blockchain based on PoSpace, that is secure under dynamic availability, is known. In this work, we prove that without additional assumptions no such protocol exists. We exactly quantify this impossibility result by proving a bound on the length of the fork required for double spending as a function of the adversarial capabilities. This bound holds for any chain selection rule, and we also show a chain selection rule (albeit a very strange one) that almost matches this bound.\r\nThe Nakamoto consensus protocol underlying the Bitcoin blockchain uses proof of work as a voting mechanism. Honest miners who contribute hashing power towards securing the chain try to extend the longest chain they are aware of. Despite its simplicity, Nakamoto consensus achieves meaningful security guarantees assuming that at any point in time, a majority of the hashing power is controlled by honest parties. This also holds under “resource variability”, i.e., if the total hashing power varies greatly over time.\r\n\r\nProofs of space (PoSpace) have been suggested as a more sustainable replacement for proofs of work. Unfortunately, no construction of a “longest-chain” blockchain based on PoSpace, that is secure under dynamic availability, is known. In this work, we prove that without additional assumptions no such protocol exists. We exactly quantify this impossibility result by proving a bound on the length of the fork required for double spending as a function of the adversarial capabilities. This bound holds for any chain selection rule, and we also show a chain selection rule (albeit a very strange one) that almost matches this bound.\r\n\r\nConcretely, we consider a security game in which the honest parties at any point control 0 > 1\r\n times more space than the adversary. The adversary can change the honest space by a factor 1+- E with every block (dynamic availability), and “replotting” the space (which allows answering two challenges using the same space) takes as much time as p blocks.\r\nWe prove that no matter what chain selection rule is used, in this game the adversary can create a fork of length o^2 . p/E that will be picked as the winner by the chain selection rule.\r\nWe also provide an upper bound that matches the lower bound up to a factor o. There exists a chain selection rule (albeit a very strange one) which in the above game requires forks of length at least o . p/E\r\nOur results show the necessity of additional assumptions to create a secure PoSpace based longest-chain blockchain. The Chia network in addition to PoSpace uses a verifiable delay function. Our bounds show that an additional primitive like that is necessary."}],"month":"01","arxiv":1,"type":"conference","project":[{"grant_number":"F8509","name":"Security and Privacy by Design for Complex Systems","_id":"34a34d57-11ca-11ed-8bc3-a2688a8724e1"}],"external_id":{"arxiv":["2505.14891"]},"date_updated":"2026-04-15T08:45:18Z","year":"2026","author":[{"id":"3EDE6DE4-AA5A-11E9-986D-341CE6697425","full_name":"Baig, Mirza Ahad","last_name":"Baig","first_name":"Mirza Ahad"},{"orcid":"0000-0002-9139-1654","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87","full_name":"Pietrzak, Krzysztof Z","first_name":"Krzysztof Z","last_name":"Pietrzak"}],"publication":"29th International Conference on Financial Cryptography and Data Security","status":"public","page":"127-142","citation":{"ista":"Baig MA, Pietrzak KZ. 2026. On the (in)security of Proofs-of-space based longest-chain blockchains. 29th International Conference on Financial Cryptography and Data Security. FC: Financial Cryptography and Data Security, LNCS, vol. 15752, 127–142.","short":"M.A. Baig, K.Z. Pietrzak, in:, 29th International Conference on Financial Cryptography and Data Security, Springer Nature, 2026, pp. 127–142.","chicago":"Baig, Mirza Ahad, and Krzysztof Z Pietrzak. “On the (in)Security of Proofs-of-Space Based Longest-Chain Blockchains.” In <i>29th International Conference on Financial Cryptography and Data Security</i>, 15752:127–42. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-07035-7_8\">https://doi.org/10.1007/978-3-032-07035-7_8</a>.","ama":"Baig MA, Pietrzak KZ. On the (in)security of Proofs-of-space based longest-chain blockchains. In: <i>29th International Conference on Financial Cryptography and Data Security</i>. Vol 15752. Springer Nature; 2026:127-142. doi:<a href=\"https://doi.org/10.1007/978-3-032-07035-7_8\">10.1007/978-3-032-07035-7_8</a>","ieee":"M. A. Baig and K. Z. Pietrzak, “On the (in)security of Proofs-of-space based longest-chain blockchains,” in <i>29th International Conference on Financial Cryptography and Data Security</i>, Miyakojima, Japan, 2026, vol. 15752, pp. 127–142.","mla":"Baig, Mirza Ahad, and Krzysztof Z. Pietrzak. “On the (in)Security of Proofs-of-Space Based Longest-Chain Blockchains.” <i>29th International Conference on Financial Cryptography and Data Security</i>, vol. 15752, Springer Nature, 2026, pp. 127–42, doi:<a href=\"https://doi.org/10.1007/978-3-032-07035-7_8\">10.1007/978-3-032-07035-7_8</a>.","apa":"Baig, M. A., &#38; Pietrzak, K. Z. (2026). On the (in)security of Proofs-of-space based longest-chain blockchains. In <i>29th International Conference on Financial Cryptography and Data Security</i> (Vol. 15752, pp. 127–142). Miyakojima, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-07035-7_8\">https://doi.org/10.1007/978-3-032-07035-7_8</a>"},"OA_type":"green","scopus_import":"1","conference":{"location":"Miyakojima, Japan","name":"FC: Financial Cryptography and Data Security","start_date":"2025-04-14","end_date":"2025-04-18"},"publisher":"Springer Nature","volume":15752,"alternative_title":["LNCS"],"day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","quality_controlled":"1","oa":1},{"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"quality_controlled":"1","oa":1,"volume":15931,"day":"01","alternative_title":["LNCS"],"OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","publication":"37th International Conference on Computer Aided Verification","page":"281-295","citation":{"chicago":"Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko. “Introducing Certificates to the Hardware Model Checking Competition.” In <i>37th International Conference on Computer Aided Verification</i>, 15931:281–95. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">https://doi.org/10.1007/978-3-031-98668-0_14</a>.","ista":"Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates to the hardware model checking competition. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.","short":"N. Froleyks, E. Yu, M. Preiner, A. Biere, K. Heljanko, in:, 37th International Conference on Computer Aided Verification, Springer Nature, 2025, pp. 281–295.","mla":"Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking Competition.” <i>37th International Conference on Computer Aided Verification</i>, vol. 15931, Springer Nature, 2025, pp. 281–95, doi:<a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">10.1007/978-3-031-98668-0_14</a>.","apa":"Froleyks, N., Yu, E., Preiner, M., Biere, A., &#38; Heljanko, K. (2025). Introducing certificates to the hardware model checking competition. In <i>37th International Conference on Computer Aided Verification</i> (Vol. 15931, pp. 281–295). Zagreb, Croatia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">https://doi.org/10.1007/978-3-031-98668-0_14</a>","ieee":"N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates to the hardware model checking competition,” in <i>37th International Conference on Computer Aided Verification</i>, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.","ama":"Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates to the hardware model checking competition. In: <i>37th International Conference on Computer Aided Verification</i>. Vol 15931. Springer Nature; 2025:281-295. doi:<a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">10.1007/978-3-031-98668-0_14</a>"},"OA_type":"hybrid","ddc":["000"],"conference":{"name":"CAV: Computer Aided Verification","start_date":"2025-07-23","end_date":"2025-07-25","location":"Zagreb, Croatia"},"publisher":"Springer Nature","file":[{"access_level":"open_access","date_updated":"2025-09-02T05:46:10Z","success":1,"date_created":"2025-09-02T05:46:10Z","file_size":1078274,"content_type":"application/pdf","checksum":"15ec1bc9b9409d3b2736f4c9d5f42fd1","file_name":"2025_CAV_Froleyks.pdf","creator":"dernst","file_id":"20266","relation":"main_file"}],"ec_funded":1,"scopus_import":"1","has_accepted_license":"1","date_updated":"2025-12-01T12:34:05Z","author":[{"first_name":"Nils","last_name":"Froleyks","full_name":"Froleyks, Nils"},{"id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","orcid":"0000-0002-4993-773X","first_name":"Zhengqi","last_name":"Yu","full_name":"Yu, Zhengqi"},{"full_name":"Preiner, Mathias","first_name":"Mathias","last_name":"Preiner"},{"full_name":"Biere, Armin","first_name":"Armin","last_name":"Biere"},{"first_name":"Keijo","last_name":"Heljanko","full_name":"Heljanko, Keijo"}],"year":"2025","publication_identifier":{"isbn":["9783031986673"],"eissn":["1611-3349"],"issn":["0302-9743"]},"acknowledgement":"This work is supported in part by the ERC-2020-AdG 101020093, the LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland under the project 336092, and a gift from Intel Corporation.\r\nFurthermore we of course also owe a big thank-you to the submitters of model checkers and benchmarks to the competition over all these years. Without their enthusiasm and support neither the competition nor this study would exist.","type":"conference","month":"01","file_date_updated":"2025-09-02T05:46:10Z","abstract":[{"lang":"eng","text":"Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency."}],"external_id":{"isi":["001562507100014"]},"project":[{"call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"title":"Introducing certificates to the hardware model checking competition","doi":"10.1007/978-3-031-98668-0_14","oa_version":"Published Version","date_created":"2025-08-17T22:01:36Z","article_processing_charge":"Yes (in subscription journal)","department":[{"_id":"ToHe"}],"intvolume":"     15931","publication_status":"published","language":[{"iso":"eng"}],"date_published":"2025-01-01T00:00:00Z","isi":1,"_id":"20189"},{"title":"Supermartingale certificates for quantitative omega-regular verification and control","article_processing_charge":"Yes (in subscription journal)","doi":"10.1007/978-3-031-98679-6_2","oa_version":"Published Version","date_created":"2025-08-24T22:01:31Z","department":[{"_id":"ToHe"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031986789"]},"acknowledgement":"This work was supported in part by the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SIS-SMU-100) and the ERC project ERC-2020-AdG 101020093.","abstract":[{"lang":"eng","text":"We present the first supermartingale certificate for quantitative \r\n-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that specifies the property of interest; hence we call it a limit-deterministic Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied only to quantitative reachability, safety, or reach-avoid properties, and to qualitative (i.e., probability 1) \r\n-regular properties.We also present fully automated algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic system dynamics and the controller can be represented in terms of polynomial inequalities. Our experiments demonstrate the ability of our method to solve verification and control tasks for stochastic systems that were beyond the reach of previous supermartingale-based approaches."}],"file_date_updated":"2025-09-02T07:34:33Z","month":"07","type":"conference","arxiv":1,"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"external_id":{"arxiv":["2505.18833"],"isi":["001562506600002"]},"date_published":"2025-07-22T00:00:00Z","isi":1,"_id":"20225","publication_status":"published","intvolume":"     15932","language":[{"iso":"eng"}],"volume":15932,"alternative_title":["LNCS"],"day":"22","OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"quality_controlled":"1","oa":1,"date_updated":"2025-12-01T12:34:41Z","year":"2025","author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","first_name":"Kaushik","full_name":"Mallik, Kaushik"},{"full_name":"Sadeghi, Pouya","last_name":"Sadeghi","first_name":"Pouya"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde"}],"publication":"37th International Conference on Computer Aided Verification","status":"public","ddc":["000"],"OA_type":"hybrid","citation":{"chicago":"Henzinger, Thomas A, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic. “Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.” In <i>37th International Conference on Computer Aided Verification</i>, 15932:29–55. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">https://doi.org/10.1007/978-3-031-98679-6_2</a>.","ista":"Henzinger TA, Mallik K, Sadeghi P, Zikelic D. 2025. Supermartingale certificates for quantitative omega-regular verification and control. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15932, 29–55.","short":"T.A. Henzinger, K. Mallik, P. Sadeghi, D. Zikelic, in:, 37th International Conference on Computer Aided Verification, Springer Nature, 2025, pp. 29–55.","ieee":"T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates for quantitative omega-regular verification and control,” in <i>37th International Conference on Computer Aided Verification</i>, Zagreb, Croatia, 2025, vol. 15932, pp. 29–55.","ama":"Henzinger TA, Mallik K, Sadeghi P, Zikelic D. Supermartingale certificates for quantitative omega-regular verification and control. In: <i>37th International Conference on Computer Aided Verification</i>. Vol 15932. Springer Nature; 2025:29-55. doi:<a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">10.1007/978-3-031-98679-6_2</a>","mla":"Henzinger, Thomas A., et al. “Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.” <i>37th International Conference on Computer Aided Verification</i>, vol. 15932, Springer Nature, 2025, pp. 29–55, doi:<a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">10.1007/978-3-031-98679-6_2</a>.","apa":"Henzinger, T. A., Mallik, K., Sadeghi, P., &#38; Zikelic, D. (2025). Supermartingale certificates for quantitative omega-regular verification and control. In <i>37th International Conference on Computer Aided Verification</i> (Vol. 15932, pp. 29–55). Zagreb, Croatia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">https://doi.org/10.1007/978-3-031-98679-6_2</a>"},"page":"29-55","has_accepted_license":"1","ec_funded":1,"scopus_import":"1","publisher":"Springer Nature","conference":{"location":"Zagreb, Croatia","end_date":"2025-07-25","start_date":"2025-07-23","name":"CAV: Computer Aided Verification"},"file":[{"content_type":"application/pdf","checksum":"beb1e2637de5b2268cc2262119439113","file_size":884831,"access_level":"open_access","date_updated":"2025-09-02T07:34:33Z","date_created":"2025-09-02T07:34:33Z","success":1,"file_name":"2025_CAV_HenzingerT.pdf","creator":"dernst","file_id":"20272","relation":"main_file"}]},{"date_updated":"2025-11-10T08:06:27Z","author":[{"full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"},{"last_name":"Weininger","first_name":"Maximilian","full_name":"Weininger, Maximilian","orcid":"0000-0002-0163-2152","id":"02ab0197-cc70-11ed-ab61-918e71f56881"},{"full_name":"Wienhöft, Patrick","last_name":"Wienhöft","first_name":"Patrick"}],"year":"2025","page":"195-218","citation":{"chicago":"Meggendorfer, Tobias, Maximilian Weininger, and Patrick Wienhöft. “What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes.” In <i>Second International Joint Conference on QEST+FORMATS</i>, 16143:195–218. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05792-1_11\">https://doi.org/10.1007/978-3-032-05792-1_11</a>.","short":"T. Meggendorfer, M. Weininger, P. Wienhöft, in:, Second International Joint Conference on QEST+FORMATS, Springer Nature, 2025, pp. 195–218.","ista":"Meggendorfer T, Weininger M, Wienhöft P. 2025. What are the odds? Improving statistical model checking of Markov decision processes. Second International Joint Conference on QEST+FORMATS. QEST-FORMATS: International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, LNCS, vol. 16143, 195–218.","mla":"Meggendorfer, Tobias, et al. “What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes.” <i>Second International Joint Conference on QEST+FORMATS</i>, vol. 16143, Springer Nature, 2025, pp. 195–218, doi:<a href=\"https://doi.org/10.1007/978-3-032-05792-1_11\">10.1007/978-3-032-05792-1_11</a>.","apa":"Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). What are the odds? Improving statistical model checking of Markov decision processes. In <i>Second International Joint Conference on QEST+FORMATS</i> (Vol. 16143, pp. 195–218). Aarhus, Denmark: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05792-1_11\">https://doi.org/10.1007/978-3-032-05792-1_11</a>","ieee":"T. Meggendorfer, M. Weininger, and P. Wienhöft, “What are the odds? Improving statistical model checking of Markov decision processes,” in <i>Second International Joint Conference on QEST+FORMATS</i>, Aarhus, Denmark, 2025, vol. 16143, pp. 195–218.","ama":"Meggendorfer T, Weininger M, Wienhöft P. What are the odds? Improving statistical model checking of Markov decision processes. In: <i>Second International Joint Conference on QEST+FORMATS</i>. Vol 16143. Springer Nature; 2025:195-218. doi:<a href=\"https://doi.org/10.1007/978-3-032-05792-1_11\">10.1007/978-3-032-05792-1_11</a>"},"status":"public","publication":"Second International Joint Conference on QEST+FORMATS","conference":{"location":"Aarhus, Denmark","start_date":"2025-08-26","end_date":"2025-08-28","name":"QEST-FORMATS: International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems"},"publisher":"Springer Nature","ec_funded":1,"scopus_import":"1","volume":16143,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"02","alternative_title":["LNCS"],"quality_controlled":"1","date_published":"2025-10-02T00:00:00Z","_id":"20610","intvolume":"     16143","publication_status":"published","language":[{"iso":"eng"}],"doi":"10.1007/978-3-032-05792-1_11","oa_version":"None","date_created":"2025-11-09T23:01:34Z","article_processing_charge":"No","title":"What are the odds? Improving statistical model checking of Markov decision processes","department":[{"_id":"KrCh"}],"acknowledgement":"This work was supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 10103441, the ERC Starting Grant DEUCE (101077178) and the DFG through the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy) and the DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783032057914"]},"project":[{"grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020"}],"type":"conference","month":"10","abstract":[{"lang":"eng","text":"Markov decision processes (MDPs) are a fundamental model of decision making which exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification assumes exact knowledge of the probabilities that govern the behaviour of an MDP. However, this assumption often is unrealistic, e.g. when modelling cyber-physical systems or biological processes. There, we can employ statistical model checking (SMC) to obtain an estimate of the MDP’s value (e.g. the maximal probability of reaching a goal state) that is close to the true value with high confidence (probably approximately correct). Model-based SMC algorithms sample the MDP and build a model of it by estimating all transition probabilities, essentially for every transition answering the question: “What are the odds?” However, so far the statistical methods employed by state-of-the-art SMC verification algorithms are quite naive or even compromise the correctness guarantees.\r\n\r\nOur first contribution is to survey, categorize, and analyse statistical methods, identifying those few that are most efficient and that provide suitable guarantees for the verification setting. Secondly, we propose improvements that exploit structural knowledge of the MDP. Both contributions generalize to many types of problem statements as they are largely independent of the setting. Moreover, our experimental evaluation shows that they lead to significant gains, reducing the number of samples that an SMC algorithm has to collect by up to two orders of magnitude."}]},{"_id":"20648","date_published":"2025-10-26T00:00:00Z","language":[{"iso":"eng"}],"publication_status":"published","intvolume":"     16145","department":[{"_id":"KrCh"}],"title":"PolyQEnt: A polynomial quantified entailment solver","article_processing_charge":"No","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2408.03796","open_access":"1"}],"doi":"10.1007/978-3-032-08707-2_19","oa_version":"Preprint","date_created":"2025-11-16T23:01:24Z","abstract":[{"lang":"eng","text":"Polynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is a tool for solving polynomial quantified entailments in which variables on both sides of the implication are real valued or unbounded integers. Our tool provides a unified framework for polynomial quantified entailment problems that arise in several papers in the literature. Our experimental evaluation over a wide range of benchmarks shows the applicability of the tool as well as its benefits as opposed to simply using existing SMT solvers to solve such constraints."}],"arxiv":1,"month":"10","type":"conference","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"external_id":{"arxiv":["2408.03796"]},"publication_identifier":{"isbn":["9783032087065"],"issn":["0302-9743"],"eissn":["1611-3349"]},"corr_author":"1","acknowledgement":"This work was supported by the following grants: ERC CoG 863818 (ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, ERC StG 101222524 (SPES), the Ethereum Foundation Research Grant FY24-1793, and the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SISSMU-100).","year":"2025","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Goharshady, Amir Kafshdar","last_name":"Goharshady","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kafshdar Goharshadi, Ehsan","last_name":"Kafshdar Goharshadi","first_name":"Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587"},{"full_name":"Karrabi, Mehrdad","last_name":"Karrabi","first_name":"Mehrdad","id":"67638922-f394-11eb-9cf6-f20423e08757","orcid":"0009-0007-5253-9170"},{"first_name":"Milad","last_name":"Saadat","full_name":"Saadat, Milad"},{"full_name":"Seeliger, Maximilian","last_name":"Seeliger","first_name":"Maximilian"},{"last_name":"Zikelic","first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2025-11-24T13:11:10Z","ec_funded":1,"scopus_import":"1","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2025-10-31","start_date":"2025-10-27","location":"Bengaluru, India"},"publisher":"Springer Nature","status":"public","publication":"23rd International Symposium on Automated Technology for Verification and Analysis","citation":{"chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, and Dorde Zikelic. “PolyQEnt: A Polynomial Quantified Entailment Solver.” In <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, 16145:411–24. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">https://doi.org/10.1007/978-3-032-08707-2_19</a>.","short":"K. Chatterjee, A.K. Goharshady, E. Goharshady, M. Karrabi, M. Saadat, M. Seeliger, D. Zikelic, in:, 23rd International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2025, pp. 411–424.","ista":"Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Saadat M, Seeliger M, Zikelic D. 2025. PolyQEnt: A polynomial quantified entailment solver. 23rd International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 16145, 411–424.","apa":"Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., Saadat, M., Seeliger, M., &#38; Zikelic, D. (2025). PolyQEnt: A polynomial quantified entailment solver. In <i>23rd International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 16145, pp. 411–424). Bengaluru, India: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">https://doi.org/10.1007/978-3-032-08707-2_19</a>","mla":"Chatterjee, Krishnendu, et al. “PolyQEnt: A Polynomial Quantified Entailment Solver.” <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, vol. 16145, Springer Nature, 2025, pp. 411–24, doi:<a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">10.1007/978-3-032-08707-2_19</a>.","ieee":"K. Chatterjee <i>et al.</i>, “PolyQEnt: A polynomial quantified entailment solver,” in <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>, Bengaluru, India, 2025, vol. 16145, pp. 411–424.","ama":"Chatterjee K, Goharshady AK, Goharshady E, et al. PolyQEnt: A polynomial quantified entailment solver. In: <i>23rd International Symposium on Automated Technology for Verification and Analysis</i>. Vol 16145. Springer Nature; 2025:411-424. doi:<a href=\"https://doi.org/10.1007/978-3-032-08707-2_19\">10.1007/978-3-032-08707-2_19</a>"},"OA_type":"green","page":"411-424","alternative_title":["LNCS"],"day":"26","OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":16145,"quality_controlled":"1","oa":1},{"language":[{"iso":"eng"}],"publication_status":"published","intvolume":"     16296","_id":"20658","date_published":"2025-11-01T00:00:00Z","abstract":[{"text":"The medial axis of a smoothly embedded surface in R^3 consists of all points for which the Euclidean distance function on the surface has at least two global minima. We generalize this notion to the mid-sphere axis, which consists of all points for which the Euclidean distance function has two interchanging saddles that swap their partners in the pairing by persistent homology. It offers a discrete-algebraic multi-scale approach to computing ridge-like structures on the surface. As a proof of concept, an algorithm that computes stair-case approximations of the mid-sphere axis is provided.","lang":"eng"}],"month":"11","type":"conference","arxiv":1,"external_id":{"arxiv":["2504.14743"]},"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783032095435"]},"department":[{"_id":"HeEd"}],"title":"The mid-sphere cousin of the medial axis transform","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2504.14743"}],"doi":"10.1007/978-3-032-09544-2_10","date_created":"2025-11-23T23:01:37Z","oa_version":"Preprint","scopus_import":"1","conference":{"location":"Groningen, The Netherlands","name":"DGMM: Discrete Geometry and Mathematical Morphology","end_date":"2025-11-06","start_date":"2025-11-03"},"publisher":"Springer Nature","status":"public","publication":"4th International Joint Conference on Discrete Geometry and Mathematical Morphology","OA_type":"green","citation":{"apa":"Edelsbrunner, H., Stephenson, E. R., &#38; Thoresen, M. H. (2025). The mid-sphere cousin of the medial axis transform. In <i>4th International Joint Conference on Discrete Geometry and Mathematical Morphology</i> (Vol. 16296, pp. 133–147). Groningen, The Netherlands: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-09544-2_10\">https://doi.org/10.1007/978-3-032-09544-2_10</a>","mla":"Edelsbrunner, Herbert, et al. “The Mid-Sphere Cousin of the Medial Axis Transform.” <i>4th International Joint Conference on Discrete Geometry and Mathematical Morphology</i>, vol. 16296, Springer Nature, 2025, pp. 133–47, doi:<a href=\"https://doi.org/10.1007/978-3-032-09544-2_10\">10.1007/978-3-032-09544-2_10</a>.","ieee":"H. Edelsbrunner, E. R. Stephenson, and M. H. Thoresen, “The mid-sphere cousin of the medial axis transform,” in <i>4th International Joint Conference on Discrete Geometry and Mathematical Morphology</i>, Groningen, The Netherlands, 2025, vol. 16296, pp. 133–147.","ama":"Edelsbrunner H, Stephenson ER, Thoresen MH. The mid-sphere cousin of the medial axis transform. In: <i>4th International Joint Conference on Discrete Geometry and Mathematical Morphology</i>. Vol 16296. Springer Nature; 2025:133-147. doi:<a href=\"https://doi.org/10.1007/978-3-032-09544-2_10\">10.1007/978-3-032-09544-2_10</a>","ista":"Edelsbrunner H, Stephenson ER, Thoresen MH. 2025. The mid-sphere cousin of the medial axis transform. 4th International Joint Conference on Discrete Geometry and Mathematical Morphology. DGMM: Discrete Geometry and Mathematical Morphology, LNCS, vol. 16296, 133–147.","chicago":"Edelsbrunner, Herbert, Elizabeth R Stephenson, and Martin H Thoresen. “The Mid-Sphere Cousin of the Medial Axis Transform.” In <i>4th International Joint Conference on Discrete Geometry and Mathematical Morphology</i>, 16296:133–47. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-09544-2_10\">https://doi.org/10.1007/978-3-032-09544-2_10</a>.","short":"H. Edelsbrunner, E.R. Stephenson, M.H. Thoresen, in:, 4th International Joint Conference on Discrete Geometry and Mathematical Morphology, Springer Nature, 2025, pp. 133–147."},"page":"133-147","year":"2025","author":[{"full_name":"Edelsbrunner, Herbert","last_name":"Edelsbrunner","first_name":"Herbert","orcid":"0000-0002-9823-6833","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87"},{"id":"2D04F932-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6862-208X","full_name":"Stephenson, Elizabeth R","first_name":"Elizabeth R","last_name":"Stephenson"},{"first_name":"Martin H","last_name":"Thoresen","full_name":"Thoresen, Martin H","id":"47CB1472-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2025-11-24T10:05:11Z","quality_controlled":"1","oa":1,"alternative_title":["LNCS"],"day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","volume":16296},{"OA_type":"green","page":"251-263","citation":{"short":"E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, Engineering Safe and Trustworthy Cyber Physical Systems, Springer Nature, Cham, 2025, pp. 251–263.","ista":"Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.Information-Flow Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber Physical Systems. LNCS, vol. 15471, 251–263.","chicago":"Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Information-Flow Interfaces and Security Lattices.” In <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>, 15471:251–63. Cham: Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">https://doi.org/10.1007/978-3-031-97537-0_15</a>.","apa":"Bartocci, E., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2025). Information-Flow Interfaces and Security Lattices. In <i>Engineering Safe and Trustworthy Cyber Physical Systems</i> (Vol. 15471, pp. 251–263). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">https://doi.org/10.1007/978-3-031-97537-0_15</a>","ama":"Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-Flow Interfaces and Security Lattices. In: <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>. Vol 15471. Cham: Springer Nature; 2025:251-263. doi:<a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">10.1007/978-3-031-97537-0_15</a>","mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces and Security Lattices.” <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>, vol. 15471, Springer Nature, 2025, pp. 251–63, doi:<a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">10.1007/978-3-031-97537-0_15</a>.","ieee":"E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-Flow Interfaces and Security Lattices,” in <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>, vol. 15471, Cham: Springer Nature, 2025, pp. 251–263."},"status":"public","publication":"Engineering Safe and Trustworthy Cyber Physical Systems","scopus_import":"1","ec_funded":1,"publisher":"Springer Nature","date_updated":"2025-12-09T07:57:55Z","year":"2025","author":[{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","last_name":"Nickovic","first_name":"Dejan"},{"last_name":"Oliveira da Costa","first_name":"Ana","full_name":"Oliveira da Costa, Ana","orcid":"0000-0002-8741-5799","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4"}],"oa":1,"quality_controlled":"1","volume":15471,"OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"day":"02","publication_status":"published","intvolume":"     15471","language":[{"iso":"eng"}],"date_published":"2025-10-02T00:00:00Z","_id":"20723","corr_author":"1","acknowledgement":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502 and by the ERC-2020-AdG 101020093.","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031975363"],"eisbn":["9783031975370"]},"place":"Cham","project":[{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"},{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"external_id":{"arxiv":["2406.14374"]},"abstract":[{"text":"Information-flow interfaces is a formalism recently proposed for specifying, composing, and refining system-wide security requirements. In this work, we show how the widely used concept of security lattices provides a natural semantic interpretation for information-flow interfaces.","lang":"eng"}],"month":"10","arxiv":1,"type":"book_chapter","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2406.14374"}],"doi":"10.1007/978-3-031-97537-0_15","date_created":"2025-12-01T15:44:58Z","oa_version":"Preprint","title":"Information-Flow Interfaces and Security Lattices","department":[{"_id":"ToHe"}]},{"year":"2025","author":[{"first_name":"Muqsit","last_name":"Azeem","full_name":"Azeem, Muqsit"},{"last_name":"Chakraborty","first_name":"Debraj","full_name":"Chakraborty, Debraj"},{"full_name":"Kanav, Sudeep","first_name":"Sudeep","last_name":"Kanav"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan"},{"full_name":"Mohagheghi, Mohammadsadegh","first_name":"Mohammadsadegh","last_name":"Mohagheghi"},{"first_name":"Stefanie","last_name":"Mohr","full_name":"Mohr, Stefanie"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","last_name":"Weininger","first_name":"Maximilian","full_name":"Weininger, Maximilian"}],"date_updated":"2025-09-30T10:46:54Z","ec_funded":1,"scopus_import":"1","conference":{"location":"Denver, CO, United States","start_date":"2025-01-20","end_date":"2025-01-21","name":"VMCAI: Verification, Model Checking, and Abstract Interpretation"},"publisher":"Springer Nature","citation":{"ama":"Azeem M, Chakraborty D, Kanav S, et al. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In: <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>. Vol 15530. Springer Nature; 2025:97-120. doi:<a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">10.1007/978-3-031-82703-7_5</a>","ieee":"M. Azeem <i>et al.</i>, “1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization,” in <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, Denver, CO, United States, 2025, vol. 15530, pp. 97–120.","apa":"Azeem, M., Chakraborty, D., Kanav, S., Kretinsky, J., Mohagheghi, M., Mohr, S., &#38; Weininger, M. (2025). 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i> (Vol. 15530, pp. 97–120). Denver, CO, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">https://doi.org/10.1007/978-3-031-82703-7_5</a>","mla":"Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, vol. 15530, Springer Nature, 2025, pp. 97–120, doi:<a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">10.1007/978-3-031-82703-7_5</a>.","short":"M. Azeem, D. Chakraborty, S. Kanav, J. Kretinsky, M. Mohagheghi, S. Mohr, M. Weininger, in:, 26th International Conference on Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2025, pp. 97–120.","ista":"Azeem M, Chakraborty D, Kanav S, Kretinsky J, Mohagheghi M, Mohr S, Weininger M. 2025. 1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. 26th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 15530, 97–120.","chicago":"Azeem, Muqsit, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh Mohagheghi, Stefanie Mohr, and Maximilian Weininger. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” In <i>26th International Conference on Verification, Model Checking, and Abstract Interpretation</i>, 15530:97–120. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-82703-7_5\">https://doi.org/10.1007/978-3-031-82703-7_5</a>."},"page":"97-120","OA_type":"green","status":"public","publication":"26th International Conference on Verification, Model Checking, and Abstract Interpretation","OA_place":"repository","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","alternative_title":["LNCS"],"day":"23","volume":15530,"oa":1,"quality_controlled":"1","_id":"19375","isi":1,"date_published":"2025-01-23T00:00:00Z","language":[{"iso":"eng"}],"publication_status":"published","intvolume":"     15530","department":[{"_id":"KrCh"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2410.18293","open_access":"1"}],"article_processing_charge":"No","date_created":"2025-03-09T23:01:29Z","doi":"10.1007/978-3-031-82703-7_5","oa_version":"Preprint","title":"1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413","name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020"}],"external_id":{"isi":["001446577100005"],"arxiv":["2410.18293"]},"abstract":[{"text":"Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs.\r\n\r\nThe idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.","lang":"eng"}],"arxiv":1,"month":"01","type":"conference","acknowledgement":"This research was funded in part by the DFG project 427755713 GOPro, the DFG GRK 2428 (ConVeY), the MUNI Award in Science and Humanities (MUNI/I/1757/2021) of the Grant Agency of Masaryk University, and the EU under MSCA grant agreement 101034413 (IST-BRIDGE).","publication_identifier":{"isbn":["9783031827020"],"issn":["0302-9743"],"eissn":["1611-3349"]}},{"isi":1,"_id":"19445","date_published":"2025-02-20T00:00:00Z","language":[{"iso":"eng"}],"publication_status":"published","intvolume":"     15411","department":[{"_id":"KrCh"}],"title":"Reconfiguration using generalized token jumping","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2411.12582"}],"article_processing_charge":"No","date_created":"2025-03-23T23:01:27Z","oa_version":"Preprint","doi":"10.1007/978-981-96-2845-2_16","abstract":[{"lang":"eng","text":"In reconfiguration, we are given two solutions to a graph problem, such as Vertex Cover or Dominating Set, with each solution represented by a placement of tokens on vertices of the graph. Our task is to reconfigure one into the other using small steps while ensuring the intermediate configurations of tokens are also valid solutions. The two commonly studied settings are Token Jumping and Token Sliding, which allows moving a single token to an arbitrary or an adjacent vertex, respectively.\r\n\r\nWe introduce new rules that generalize Token Jumping, parameterized by the number of tokens allowed to move at once and by the maximum distance of each move. Our main contribution is identifying minimal rules that allow reconfiguring any possible given solution into any other for Independent Set, Vertex Cover, and Dominating Set. For each minimal rule, we also provide an efficient algorithm that finds a corresponding reconfiguration sequence.\r\n\r\nWe further focus on the rule that allows each token to move to an adjacent vertex in a single step. This natural variant turns out to be the minimal rule that guarantees reconfigurability for Vertex Cover. We determine the computational complexity of deciding whether a (shortest) reconfiguration sequence exists under this rule for the three studied problems. While reachability for Vertex Cover is shown to be in P, finding a shortest sequence is shown to be NP-complete. For Independent Set and Dominating Set, even reachability is shown to be PSPACE-complete."}],"type":"conference","month":"02","arxiv":1,"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"external_id":{"isi":["001537885900016"],"arxiv":["2411.12582"]},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9789819628445"]},"acknowledgement":"J. M. Křišťan acknowledges the support of the Czech Science Foundation Grant No. 24-12046S. This work was supported by the Grant Agency of the Czech Technical University in Prague, grant No. SGS23/205/OHK3/3T/18. J. Svoboda acknowledges the support of the ERC CoG 863818 (ForM-SMArt) grant.","year":"2025","author":[{"first_name":"Jan Matyáš","last_name":"Křišťan","full_name":"Křišťan, Jan Matyáš"},{"last_name":"Svoboda","first_name":"Jakub","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425"}],"date_updated":"2025-09-30T11:14:33Z","scopus_import":"1","ec_funded":1,"conference":{"location":"Chengdu, China","end_date":"2025-03-02","start_date":"2025-02-28","name":"WALCOM: International Conference and Workshops on Algorithms and Computation"},"publisher":"Springer Nature","publication":"19th International Conference and Workshops on Algorithms and Computation","status":"public","OA_type":"green","page":"244-265","citation":{"chicago":"Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized Token Jumping.” In <i>19th International Conference and Workshops on Algorithms and Computation</i>, 15411:244–65. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">https://doi.org/10.1007/978-981-96-2845-2_16</a>.","ista":"Křišťan JM, Svoboda J. 2025. Reconfiguration using generalized token jumping. 19th International Conference and Workshops on Algorithms and Computation. WALCOM: International Conference and Workshops on Algorithms and Computation, LNCS, vol. 15411, 244–265.","short":"J.M. Křišťan, J. Svoboda, in:, 19th International Conference and Workshops on Algorithms and Computation, Springer Nature, 2025, pp. 244–265.","ama":"Křišťan JM, Svoboda J. Reconfiguration using generalized token jumping. In: <i>19th International Conference and Workshops on Algorithms and Computation</i>. Vol 15411. Springer Nature; 2025:244-265. doi:<a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">10.1007/978-981-96-2845-2_16</a>","ieee":"J. M. Křišťan and J. Svoboda, “Reconfiguration using generalized token jumping,” in <i>19th International Conference and Workshops on Algorithms and Computation</i>, Chengdu, China, 2025, vol. 15411, pp. 244–265.","apa":"Křišťan, J. M., &#38; Svoboda, J. (2025). Reconfiguration using generalized token jumping. In <i>19th International Conference and Workshops on Algorithms and Computation</i> (Vol. 15411, pp. 244–265). Chengdu, China: Springer Nature. <a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">https://doi.org/10.1007/978-981-96-2845-2_16</a>","mla":"Křišťan, Jan Matyáš, and Jakub Svoboda. “Reconfiguration Using Generalized Token Jumping.” <i>19th International Conference and Workshops on Algorithms and Computation</i>, vol. 15411, Springer Nature, 2025, pp. 244–65, doi:<a href=\"https://doi.org/10.1007/978-981-96-2845-2_16\">10.1007/978-981-96-2845-2_16</a>."},"alternative_title":["LNCS"],"day":"20","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","OA_place":"repository","volume":15411,"quality_controlled":"1","oa":1},{"volume":15263,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","day":"01","alternative_title":["LNCS"],"oa":1,"quality_controlled":"1","date_updated":"2025-11-05T07:52:35Z","author":[{"first_name":"Zeta","last_name":"Avarikioti","full_name":"Avarikioti, Zeta"},{"full_name":"Bastankhah, Mahsa","last_name":"Bastankhah","first_name":"Mahsa"},{"full_name":"Maddah-Ali, Mohammad Ali","last_name":"Maddah-Ali","first_name":"Mohammad Ali"},{"full_name":"Pietrzak, Krzysztof Z","first_name":"Krzysztof Z","last_name":"Pietrzak","orcid":"0000-0002-9139-1654","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","full_name":"Svoboda, Jakub"},{"first_name":"Michelle X","last_name":"Yeo","full_name":"Yeo, Michelle X","orcid":"0009-0001-3676-4809","id":"2D82B818-F248-11E8-B48F-1D18A9856A87"}],"year":"2025","page":"207-223","OA_type":"green","citation":{"ieee":"Z. Avarikioti, M. Bastankhah, M. A. Maddah-Ali, K. Z. Pietrzak, J. Svoboda, and M. X. Yeo, “Route discovery in private payment channel networks,” in <i>Computer Security. ESORICS 2024 International Workshops</i>, Bydgoszcz, Poland, 2025, vol. 15263, pp. 207–223.","mla":"Avarikioti, Zeta, et al. “Route Discovery in Private Payment Channel Networks.” <i>Computer Security. ESORICS 2024 International Workshops</i>, vol. 15263, Springer Nature, 2025, pp. 207–23, doi:<a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">10.1007/978-3-031-82349-7_15</a>.","apa":"Avarikioti, Z., Bastankhah, M., Maddah-Ali, M. A., Pietrzak, K. Z., Svoboda, J., &#38; Yeo, M. X. (2025). Route discovery in private payment channel networks. In <i>Computer Security. ESORICS 2024 International Workshops</i> (Vol. 15263, pp. 207–223). Bydgoszcz, Poland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">https://doi.org/10.1007/978-3-031-82349-7_15</a>","ama":"Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX. Route discovery in private payment channel networks. In: <i>Computer Security. ESORICS 2024 International Workshops</i>. Vol 15263. Springer Nature; 2025:207-223. doi:<a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">10.1007/978-3-031-82349-7_15</a>","ista":"Avarikioti Z, Bastankhah M, Maddah-Ali MA, Pietrzak KZ, Svoboda J, Yeo MX. 2025. Route discovery in private payment channel networks. Computer Security. ESORICS 2024 International Workshops. ESORICS: European Symposium on Research in Computer Security, LNCS, vol. 15263, 207–223.","chicago":"Avarikioti, Zeta, Mahsa Bastankhah, Mohammad Ali Maddah-Ali, Krzysztof Z Pietrzak, Jakub Svoboda, and Michelle X Yeo. “Route Discovery in Private Payment Channel Networks.” In <i>Computer Security. ESORICS 2024 International Workshops</i>, 15263:207–23. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-82349-7_15\">https://doi.org/10.1007/978-3-031-82349-7_15</a>.","short":"Z. Avarikioti, M. Bastankhah, M.A. Maddah-Ali, K.Z. Pietrzak, J. Svoboda, M.X. Yeo, in:, Computer Security. ESORICS 2024 International Workshops, Springer Nature, 2025, pp. 207–223."},"publication":"Computer Security. ESORICS 2024 International Workshops","status":"public","conference":{"name":"ESORICS: European Symposium on Research in Computer Security","end_date":"2024-09-20","start_date":"2024-09-16","location":"Bydgoszcz, Poland"},"publisher":"Springer Nature","ec_funded":1,"scopus_import":"1","doi":"10.1007/978-3-031-82349-7_15","oa_version":"Submitted Version","date_created":"2025-04-20T22:01:28Z","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2021/1539"}],"article_processing_charge":"No","title":"Route discovery in private payment channel networks","department":[{"_id":"KrPi"},{"_id":"KrCh"}],"acknowledgement":"This work was supported in part by the ERC CoG 863818 (ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, and MOE-T2EP20122-0014 (Data-Driven Distributed Algorithms) grants.","publication_identifier":{"isbn":["9783031823480"],"eissn":["1611-3349"],"issn":["0302-9743"]},"project":[{"call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"month":"04","type":"conference","abstract":[{"lang":"eng","text":"In this work, we explore route discovery in private payment channel networks. We first determine what “ideal\" privacy for a routing protocol means in this setting. We observe that protocols achieving this strong privacy definition exist by leveraging Multi-Party Computation but they are inherently inefficient as they must involve the entire network. We then present protocols with weaker privacy guarantees but much better efficiency (involving only a small fraction of the nodes). The core idea is that both sender and receiver gossip a message which propagates through the network, and the moment any node in the network receives both messages, a path is found. In our first protocol the message is always sent to all neighbouring nodes with a delay proportional to the fees of that edge. In our second protocol the message is only sent to one neighbour chosen randomly with a probability proportional to its degree. We additionally propose a more realistic notion of privacy in order to measure the privacy leakage of our protocols in practice. Our realistic notion of privacy challenges an adversary that join the network with a fixed budget to create channels to guess the sender and receiver of a transaction upon receiving messages from our protocols. Simulations of our protocols on the Lightning network topology (for random transactions and uniform fees) show that 1) forming edges with high degree nodes is a more effective attack strategy for the adversary, 2) there is a tradeoff between the number of nodes involved in our protocols (privacy) and the optimality of the discovered path, and 3) our protocols involve a very small fraction of the network on average."}],"date_published":"2025-04-01T00:00:00Z","_id":"19600","intvolume":"     15263","publication_status":"published","language":[{"iso":"eng"}]},{"_id":"19712","date_published":"2025-04-28T00:00:00Z","language":[{"iso":"eng"}],"publication_status":"published","intvolume":"     15606","department":[{"_id":"KrPi"}],"article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://www.research-collection.ethz.ch/handle/20.500.11850/732894"}],"doi":"10.1007/978-3-031-91095-1_14","date_created":"2025-05-19T14:15:01Z","oa_version":"Submitted Version","title":"On the soundness of algebraic attacks against code-based assumptions","abstract":[{"lang":"eng","text":"We study recent algebraic attacks (Briaud-Øygarden EC’23) on the Regular Syndrome Decoding (RSD) problem and the assumptions underlying the correctness of their attacks’ complexity estimates. By relating these assumptions to interesting algebraic-combinatorial problems, we prove that they do not hold in full generality. However, we show that they are (asymptotically) true for most parameter sets, supporting the soundness of algebraic attacks on RSD. Further, we prove—without any heuristics or assumptions—that RSD can be broken in polynomial time whenever the number of error blocks times the square of the size of error blocks is larger than 2 times the square of the dimension of the code.\r\nAdditionally, we use our methodology to attack a variant of the Learning With Errors problem where each error term lies in a fixed set of constant size. We prove that this problem can be broken in polynomial time, given a sufficient number of samples. This result improves on the seminal work by Arora and Ge (ICALP’11), as the attack’s time complexity is independent of the LWE modulus."}],"type":"conference","month":"04","corr_author":"1","acknowledgement":"We thank Pierre Briaud and Morten Øygarden for helpful discussions on algebraic attacks on RSD, and the EC reviewers for helpful comments.","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031910944"],"eisbn":["9783031910951"]},"year":"2025","author":[{"orcid":"0000-0002-2505-4246","id":"ffc563a3-f6e0-11ea-865d-e3cce03d17cc","first_name":"Miguel","last_name":"Cueto Noval","full_name":"Cueto Noval, Miguel"},{"last_name":"Merz","first_name":"Simon-Philipp","full_name":"Merz, Simon-Philipp"},{"last_name":"Stählin","first_name":"Patrick","full_name":"Stählin, Patrick"},{"orcid":"0000-0002-8929-0221","id":"f6b56fb6-dc63-11ee-9dbf-f6780863a85a","last_name":"Ünal","first_name":"Akin","full_name":"Ünal, Akin"}],"date_updated":"2025-05-28T06:12:39Z","scopus_import":"1","publisher":"Springer Nature","conference":{"name":"EUROCRYPT: International Conference on the Theory and Applications of Cryptographic Techniques","end_date":"2025-05-08","start_date":"2025-05-04","location":"Madrid, Spain"},"page":"385-415","OA_type":"green","citation":{"mla":"Cueto Noval, Miguel, et al. “On the Soundness of Algebraic Attacks against Code-Based Assumptions.” <i>44th Annual International Conference on the Theory and Applications of Cryptographic Techniques</i>, vol. 15606, Springer Nature, 2025, pp. 385–415, doi:<a href=\"https://doi.org/10.1007/978-3-031-91095-1_14\">10.1007/978-3-031-91095-1_14</a>.","apa":"Cueto Noval, M., Merz, S.-P., Stählin, P., &#38; Ünal, A. (2025). On the soundness of algebraic attacks against code-based assumptions. In <i>44th Annual International Conference on the Theory and Applications of Cryptographic Techniques</i> (Vol. 15606, pp. 385–415). Madrid, Spain: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-91095-1_14\">https://doi.org/10.1007/978-3-031-91095-1_14</a>","ama":"Cueto Noval M, Merz S-P, Stählin P, Ünal A. On the soundness of algebraic attacks against code-based assumptions. In: <i>44th Annual International Conference on the Theory and Applications of Cryptographic Techniques</i>. Vol 15606. Springer Nature; 2025:385-415. doi:<a href=\"https://doi.org/10.1007/978-3-031-91095-1_14\">10.1007/978-3-031-91095-1_14</a>","ieee":"M. Cueto Noval, S.-P. Merz, P. Stählin, and A. Ünal, “On the soundness of algebraic attacks against code-based assumptions,” in <i>44th Annual International Conference on the Theory and Applications of Cryptographic Techniques</i>, Madrid, Spain, 2025, vol. 15606, pp. 385–415.","short":"M. Cueto Noval, S.-P. Merz, P. Stählin, A. Ünal, in:, 44th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Springer Nature, 2025, pp. 385–415.","chicago":"Cueto Noval, Miguel, Simon-Philipp Merz, Patrick Stählin, and Akin Ünal. “On the Soundness of Algebraic Attacks against Code-Based Assumptions.” In <i>44th Annual International Conference on the Theory and Applications of Cryptographic Techniques</i>, 15606:385–415. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-91095-1_14\">https://doi.org/10.1007/978-3-031-91095-1_14</a>.","ista":"Cueto Noval M, Merz S-P, Stählin P, Ünal A. 2025. On the soundness of algebraic attacks against code-based assumptions. 44th Annual International Conference on the Theory and Applications of Cryptographic Techniques. EUROCRYPT: International Conference on the Theory and Applications of Cryptographic Techniques, LNCS, vol. 15606, 385–415."},"publication":"44th Annual International Conference on the Theory and Applications of Cryptographic Techniques","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","alternative_title":["LNCS"],"day":"28","volume":15606,"oa":1,"quality_controlled":"1"},{"_id":"19738","date_published":"2025-05-05T00:00:00Z","language":[{"iso":"eng"}],"intvolume":"     15677","department":[{"_id":"KrPi"},{"_id":"GradSch"}],"title":"Securely instantiating ‘Half Gates’ garbling in the standard model","doi":"10.1007/978-3-031-91829-2_2","oa_version":"Preprint","date_created":"2025-05-25T22:17:02Z","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2025/281"}],"article_processing_charge":"No","type":"conference","month":"05","abstract":[{"lang":"eng","text":"Garbling is a fundamental cryptographic primitive, with numerous theoretical and practical applications. Since the first construction by Yao (FOCS’82, ’86), a line of work has concerned itself with reducing the communication and computational complexity of that construction. One of the most efficient garbling schemes presently is the ‘Half Gates’ scheme by Zahur, Rosulek, and Evans (Eurocrypt’15). Despite its widespread adoption, the provable security of this scheme has been based on assumptions whose only instantiations are in idealized models. For example, in their original paper, Zahur, Rosulek, and Evans showed that hash functions satisfying a notion called circular correlation robustness (CCR) suffice for this task, and then proved that CCR secure hash functions can be instantiated in the random permutation model.\r\nIn this work, we show how to securely instantiate the Half Gates scheme in the standard model. To this end, we first show how this scheme can be securely instantiated given a (family of) weak CCR hash function, a notion that we introduce. Furthermore, we show how a weak CCR hash function can be used to securely instantiate other efficient garbling schemes, namely the ones by Rosulek and Roy (Crypto’21) and Heath (Eurocrypt’24). Thus we believe this notion to be of independent interest.\r\nFinally, we construct such weak CCR hash functions using indistinguishability obfuscation and one-way functions. The security proof of this construction constitutes our main technical contribution. While our construction is not practical, it serves as a proof of concept supporting the soundness of these garbling schemes, which we regard to be particularly important given the recent initiative by NIST to standardize garbling, and the optimizations in Half Gates being potentially adopted."}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031918285"]},"author":[{"first_name":"Anasuya","last_name":"Acharya","full_name":"Acharya, Anasuya"},{"first_name":"Karen","last_name":"Azari","full_name":"Azari, Karen"},{"id":"3EDE6DE4-AA5A-11E9-986D-341CE6697425","last_name":"Baig","first_name":"Mirza Ahad","full_name":"Baig, Mirza Ahad"},{"full_name":"Hofheinz, Dennis","last_name":"Hofheinz","first_name":"Dennis"},{"first_name":"Chethan","last_name":"Kamath","full_name":"Kamath, Chethan"}],"year":"2025","date_updated":"2025-06-02T07:01:45Z","publisher":"Springer Nature","conference":{"name":"PKC: Public-Key Cryptography","end_date":"2025-05-15","start_date":"2025-05-12","location":"Roros, Norway"},"scopus_import":"1","publication":"28th IACR International Conference on Practice and Theory of Public-Key Cryptography","status":"public","OA_type":"green","citation":{"short":"A. Acharya, K. Azari, M.A. Baig, D. Hofheinz, C. Kamath, in:, 28th IACR International Conference on Practice and Theory of Public-Key Cryptography, Springer Nature, 2025, pp. 37–75.","ista":"Acharya A, Azari K, Baig MA, Hofheinz D, Kamath C. 2025. Securely instantiating ‘Half Gates’ garbling in the standard model. 28th IACR International Conference on Practice and Theory of Public-Key Cryptography. PKC: Public-Key Cryptography, LNCS, vol. 15677, 37–75.","chicago":"Acharya, Anasuya, Karen Azari, Mirza Ahad Baig, Dennis Hofheinz, and Chethan Kamath. “Securely Instantiating ‘Half Gates’ Garbling in the Standard Model.” In <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i>, 15677:37–75. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-91829-2_2\">https://doi.org/10.1007/978-3-031-91829-2_2</a>.","ama":"Acharya A, Azari K, Baig MA, Hofheinz D, Kamath C. Securely instantiating ‘Half Gates’ garbling in the standard model. In: <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i>. Vol 15677. Springer Nature; 2025:37-75. doi:<a href=\"https://doi.org/10.1007/978-3-031-91829-2_2\">10.1007/978-3-031-91829-2_2</a>","mla":"Acharya, Anasuya, et al. “Securely Instantiating ‘Half Gates’ Garbling in the Standard Model.” <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i>, vol. 15677, Springer Nature, 2025, pp. 37–75, doi:<a href=\"https://doi.org/10.1007/978-3-031-91829-2_2\">10.1007/978-3-031-91829-2_2</a>.","apa":"Acharya, A., Azari, K., Baig, M. A., Hofheinz, D., &#38; Kamath, C. (2025). Securely instantiating ‘Half Gates’ garbling in the standard model. In <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i> (Vol. 15677, pp. 37–75). Roros, Norway: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-91829-2_2\">https://doi.org/10.1007/978-3-031-91829-2_2</a>","ieee":"A. Acharya, K. Azari, M. A. Baig, D. Hofheinz, and C. Kamath, “Securely instantiating ‘Half Gates’ garbling in the standard model,” in <i>28th IACR International Conference on Practice and Theory of Public-Key Cryptography</i>, Roros, Norway, 2025, vol. 15677, pp. 37–75."},"page":"37-75","day":"05","alternative_title":["LNCS"],"OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":15677,"quality_controlled":"1","oa":1},{"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"first_name":"Cedric","last_name":"Richter","full_name":"Richter, Cedric"}],"year":"2025","date_updated":"2025-06-02T07:21:41Z","conference":{"end_date":"2025-05-08","start_date":"2025-05-03","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Hamilton, ON, Canada"},"publisher":"Springer Nature","file":[{"file_id":"19766","relation":"main_file","file_name":"2025_TACAS_Chalupa.pdf","creator":"dernst","content_type":"application/pdf","checksum":"3f604f25dbe37383acb7f8308aad3ca6","file_size":259050,"date_created":"2025-06-02T07:10:35Z","success":1,"date_updated":"2025-06-02T07:10:35Z","access_level":"open_access"}],"ec_funded":1,"has_accepted_license":"1","scopus_import":"1","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","status":"public","ddc":["000"],"OA_type":"hybrid","page":"212-216","citation":{"ista":"Chalupa M, Richter C. 2025. BUBAAK: Dynamic cooperative verification. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15698, 212–216.","chicago":"Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15698:212–16. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">https://doi.org/10.1007/978-3-031-90660-2_14</a>.","short":"M. Chalupa, C. Richter, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 212–216.","mla":"Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15698, Springer Nature, 2025, pp. 212–16, doi:<a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">10.1007/978-3-031-90660-2_14</a>.","ama":"Chalupa M, Richter C. BUBAAK: Dynamic cooperative verification. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15698. Springer Nature; 2025:212-216. doi:<a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">10.1007/978-3-031-90660-2_14</a>","ieee":"M. Chalupa and C. Richter, “BUBAAK: Dynamic cooperative verification,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15698, pp. 212–216.","apa":"Chalupa, M., &#38; Richter, C. (2025). BUBAAK: Dynamic cooperative verification. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15698, pp. 212–216). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">https://doi.org/10.1007/978-3-031-90660-2_14</a>"},"day":"01","alternative_title":["LNCS"],"OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":15698,"quality_controlled":"1","oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"_id":"19739","date_published":"2025-05-01T00:00:00Z","language":[{"iso":"eng"}],"intvolume":"     15698","publication_status":"published","department":[{"_id":"ToHe"}],"title":"BUBAAK: Dynamic cooperative verification","oa_version":"Published Version","date_created":"2025-05-25T22:17:04Z","doi":"10.1007/978-3-031-90660-2_14","article_processing_charge":"No","type":"conference","file_date_updated":"2025-06-02T07:10:35Z","month":"05","abstract":[{"text":"Cooperative verification is gaining momentum in recent years. The usual setup in cooperative verification is that a verifier A is run with some pre-defined resources, and if it is not able to verify the program, the verification task is passed to a verifier B together with information learned about the program by verifier A, then the chain can continue to a verifier C, and so on. This scheme is static: tools run one after another in a fixed pre-defined order and fixed parameters and resource limits (the scheme may differ for properties to be analyzed, though).\r\n\r\nBubaak is a program analysis tool that allows to run multiple program verifiers in a dynamically changing combination of parallel and sequential portfolios. Bubaak starts the verification process by invoking an initial set of tasks; every task, when it is done (e.g., because of hitting a time limit or finishing its job), rewrites itself into one or more successor tasks. New tasks can be also spawned upon events generated by other tasks. This all happens dynamically based on the information gathered by finished and running tasks. During their execution, tasks that run in parallel can exchange (partial) verification artifacts, either directly or with Bubaak as an intermediary.","lang":"eng"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020"}],"publication_identifier":{"isbn":["9783031906596"],"eissn":["1611-3349"],"issn":["0302-9743"]},"acknowledgement":"This work was in part supported by the ERC-2020-AdG 10102009 grant, and in part by the German Research Foundation (DFG) - WE2290/13-2 (Coop2).","corr_author":"1"},{"OA_type":"hybrid","page":"217-236","citation":{"ista":"Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. 2025. Value iteration with guessing for Markov chains and Markov decision processes. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 217–236.","short":"K. Chatterjee, M. Jafariraviz, R.J. Saona Urmeneta, J. Svoboda, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 217–236.","chicago":"Chatterjee, Krishnendu, Mahdi Jafariraviz, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Value Iteration with Guessing for Markov Chains and Markov Decision Processes.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:217–36. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">https://doi.org/10.1007/978-3-031-90653-4_11</a>.","mla":"Chatterjee, Krishnendu, et al. “Value Iteration with Guessing for Markov Chains and Markov Decision Processes.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 217–36, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">10.1007/978-3-031-90653-4_11</a>.","apa":"Chatterjee, K., Jafariraviz, M., Saona Urmeneta, R. J., &#38; Svoboda, J. (2025). Value iteration with guessing for Markov chains and Markov decision processes. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 217–236). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">https://doi.org/10.1007/978-3-031-90653-4_11</a>","ieee":"K. Chatterjee, M. Jafariraviz, R. J. Saona Urmeneta, and J. Svoboda, “Value iteration with guessing for Markov chains and Markov decision processes,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 217–236.","ama":"Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. Value iteration with guessing for Markov chains and Markov decision processes. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:217-236. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">10.1007/978-3-031-90653-4_11</a>"},"ddc":["000"],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","status":"public","ec_funded":1,"scopus_import":"1","has_accepted_license":"1","file":[{"file_id":"19767","relation":"main_file","file_name":"2025_TACAS_Chatterjee.pdf","creator":"dernst","content_type":"application/pdf","checksum":"45da6efbcbed20aada16c48c8e55e2d6","file_size":557481,"success":1,"date_created":"2025-06-02T07:31:12Z","access_level":"open_access","date_updated":"2025-06-02T07:31:12Z"}],"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2025-05-08","start_date":"2025-05-03","location":"Hamilton, ON, Canada"},"publisher":"Springer Nature","date_updated":"2025-06-02T07:35:06Z","year":"2025","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Jafariraviz, Mahdi","first_name":"Mahdi","last_name":"Jafariraviz"},{"last_name":"Saona Urmeneta","first_name":"Raimundo J","full_name":"Saona Urmeneta, Raimundo J","orcid":"0000-0001-5103-038X","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425"},{"orcid":"0000-0002-1419-3267","id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","first_name":"Jakub","last_name":"Svoboda","full_name":"Svoboda, Jakub"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"quality_controlled":"1","volume":15697,"OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"day":"01","publication_status":"published","intvolume":"     15697","language":[{"iso":"eng"}],"date_published":"2025-05-01T00:00:00Z","_id":"19740","corr_author":"1","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and Austrian Science Fund (FWF) 10.55776/COE12 grant.","publication_identifier":{"isbn":["9783031906527"],"eissn":["1611-3349"],"issn":["0302-9743"]},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"external_id":{"arxiv":["2505.06769"]},"abstract":[{"text":"Two standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature.","lang":"eng"}],"type":"conference","month":"05","file_date_updated":"2025-06-02T07:31:12Z","arxiv":1,"article_processing_charge":"No","date_created":"2025-05-25T22:17:06Z","oa_version":"Published Version","doi":"10.1007/978-3-031-90653-4_11","title":"Value iteration with guessing for Markov chains and Markov decision processes","department":[{"_id":"KrCh"}]},{"scopus_import":"1","has_accepted_license":"1","ec_funded":1,"conference":{"end_date":"2025-05-08","start_date":"2025-05-03","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Hamilton, ON, Canada"},"file":[{"date_created":"2025-06-02T09:35:42Z","success":1,"access_level":"open_access","date_updated":"2025-06-02T09:35:42Z","content_type":"application/pdf","file_size":711271,"checksum":"d45856b503b1dd4f8f14c3566327225b","file_id":"19770","relation":"main_file","file_name":"2025_TACAS_Budde.pdf","creator":"dernst"}],"publisher":"Springer Nature","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","status":"public","ddc":["000"],"citation":{"short":"C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 167–190.","ista":"Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound statistical model checking for probabilities and expected rewards. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15696, 167–190.","chicago":"Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:167–90. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>.","ama":"Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical model checking for probabilities and expected rewards. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer Nature; 2025:167-190. doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">10.1007/978-3-031-90643-5_9</a>","mla":"Budde, Carlos E., et al. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 167–90, doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">10.1007/978-3-031-90643-5_9</a>.","apa":"Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). Sound statistical model checking for probabilities and expected rewards. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>","ieee":"C. E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft, “Sound statistical model checking for probabilities and expected rewards,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15696, pp. 167–190."},"page":"167-190","OA_type":"hybrid","year":"2025","author":[{"last_name":"Budde","first_name":"Carlos E.","full_name":"Budde, Carlos E."},{"full_name":"Hartmanns, Arnd","first_name":"Arnd","last_name":"Hartmanns"},{"last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"},{"id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian","last_name":"Weininger","first_name":"Maximilian"},{"last_name":"Wienhöft","first_name":"Patrick","full_name":"Wienhöft, Patrick"}],"date_updated":"2025-06-02T09:45:41Z","quality_controlled":"1","oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"alternative_title":["LNCS"],"day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"publisher","volume":15696,"language":[{"iso":"eng"}],"publication_status":"published","intvolume":"     15696","related_material":{"record":[{"relation":"research_data","id":"19769","status":"public"}]},"_id":"19742","date_published":"2025-05-01T00:00:00Z","abstract":[{"text":"Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The modes SMC tool implements our methods and recommendations, which we use to experimentally confirm our results.","lang":"eng"}],"type":"conference","arxiv":1,"month":"05","file_date_updated":"2025-06-02T09:35:42Z","project":[{"_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","call_identifier":"H2020"}],"external_id":{"arxiv":["2411.00559"]},"publication_identifier":{"isbn":["9783031906428"],"eissn":["1611-3349"],"issn":["0302-9743"]},"acknowledgement":"This work was supported by the DFG through the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy) and the TRR 248 (see perspicuous-computing.science, project ID 389792660), by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED), by the EU under NextGenerationEU projects D53D23008400006 (Smartitude) under MUR PRIN 2022 and PE00000014 (SERICS) under MUR PNRR, by the Interreg North Sea project STORM_SAFE, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy).","department":[{"_id":"KrCh"}],"title":"Sound statistical model checking for probabilities and expected rewards","article_processing_charge":"No","doi":"10.1007/978-3-031-90643-5_9","oa_version":"Published Version","date_created":"2025-05-25T22:17:08Z"}]