[{"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"acknowledgement":"This work was partially supported by the ERC-2020-AdG 10102009 grant.","intvolume":"     14572","ddc":["000"],"has_accepted_license":"1","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"first_name":"Cedric","last_name":"Richter","full_name":"Richter, Cedric"}],"date_created":"2024-04-20T18:14:06Z","publication_identifier":{"eissn":["1611-3349"],"eisbn":["9783031572562"],"issn":["0302-9743"],"isbn":["9783031572555"]},"alternative_title":["LNCS"],"_id":"15333","article_processing_charge":"Yes (in subscription journal)","publication_status":"published","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Luxembourg City, Luxembourg","end_date":"2024-04-11","start_date":"2024-04-06"},"doi":"10.1007/978-3-031-57256-2_20","department":[{"_id":"ToHe"}],"file_date_updated":"2024-04-26T11:27:26Z","abstract":[{"lang":"eng","text":"BUBAAK-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top of BUBAAK, a tool designed for running combinations of verifiers in parallel. In contrast to BUBAAK, that directly invokes verifiers on the inputs, BUBAAK-SpLit first starts by splitting the input program into multiple modified versions called program splits. During the splitting process, BUBAAK-SpLit utilizes a weak verifier (in our case symbolic execution with a short timelimit) to analyze each generated program split. If the weak verifier fails on a program split, we split this program split again and start the verification process again on the generated program splits. We run the splitting process until a predefined number of hard-to-verify program splits is generated or a splitting limit is reached. During the main verification phase, we run a combination of BUBAAK-LEE and SLOWBEAST in parallel on the remaining unsolved parts of the verification task."}],"ec_funded":1,"scopus_import":"1","status":"public","page":"353–358","file":[{"file_size":577128,"checksum":"208c855c60824bec936b8d01d0396474","content_type":"application/pdf","file_id":"15347","success":1,"access_level":"open_access","file_name":"2024_LNCS_Chalupa.pdf","date_updated":"2024-04-26T11:27:26Z","relation":"main_file","creator":"cchlebak","date_created":"2024-04-26T11:27:26Z"}],"citation":{"ieee":"M. Chalupa and C. Richter, “Bubaak-SpLit: Split what you cannot verify (Competition contribution),” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 353–358.","mla":"Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 353–358, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">10.1007/978-3-031-57256-2_20</a>.","short":"M. Chalupa, C. Richter, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 353–358.","chicago":"Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:353–358. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">https://doi.org/10.1007/978-3-031-57256-2_20</a>.","ista":"Chalupa M, Richter C. 2024. Bubaak-SpLit: Split what you cannot verify (Competition contribution). 30th 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. 14572, 353–358.","ama":"Chalupa M, Richter C. Bubaak-SpLit: Split what you cannot verify (Competition contribution). In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:353–358. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">10.1007/978-3-031-57256-2_20</a>","apa":"Chalupa, M., &#38; Richter, C. (2024). Bubaak-SpLit: Split what you cannot verify (Competition contribution). In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 353–358). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">https://doi.org/10.1007/978-3-031-57256-2_20</a>"},"quality_controlled":"1","oa_version":"Published Version","day":"05","external_id":{"isi":["001284187100020"]},"oa":1,"title":"Bubaak-SpLit: Split what you cannot verify (Competition contribution)","corr_author":"1","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","type":"conference","isi":1,"publisher":"Springer Nature","date_published":"2024-04-05T00:00:00Z","language":[{"iso":"eng"}],"date_updated":"2025-09-04T13:48:25Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"year":"2024","month":"04","volume":14572,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345"},{"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"intvolume":"     14572","acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093 and by ISF grant no. 1679/21.","author":[{"full_name":"Avni, Guy","first_name":"Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Kaushik","last_name":"Mallik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik"},{"full_name":"Sadhukhan, Suman","last_name":"Sadhukhan","first_name":"Suman"}],"date_created":"2024-05-12T22:01:02Z","ddc":["000"],"has_accepted_license":"1","publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031572555"]},"_id":"15376","article_processing_charge":"Yes (in subscription journal)","alternative_title":["LNCS"],"file_date_updated":"2024-05-22T07:09:24Z","ec_funded":1,"abstract":[{"text":"Sequential decision-making tasks often require satisfaction of multiple, partially-contradictory objectives. Existing approaches are monolithic, where a single policy fulfills all objectives. We present auction-based scheduling, a decentralized framework for multi-objective sequential decision making. Each objective is fulfilled using a separate and independent policy. Composition of policies is performed at runtime, where at each step, the policies simultaneously bid from pre-allocated budgets for the privilege of choosing the next action. The framework allows policies to be independently created, modified, and replaced. We study path planning problems on finite graphs with two temporal objectives and present algorithms to synthesize policies together with bidding policies in a decentralized manner. We consider three categories of decentralized synthesis problems, parameterized by the assumptions that the policies make on each other. We identify a class of assumptions called assume-admissible for which synthesis is always possible for graphs whose every vertex has at most two outgoing edges.","lang":"eng"}],"scopus_import":"1","conference":{"location":"Luxembourg City, Luxembourg","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2024-04-11","start_date":"2024-04-06"},"doi":"10.1007/978-3-031-57256-2_8","department":[{"_id":"ToHe"}],"page":"153-172","file":[{"file_size":508191,"content_type":"application/pdf","checksum":"dbeb123510997886d11925aedbf9c400","creator":"dernst","date_created":"2024-05-22T07:09:24Z","access_level":"open_access","success":1,"file_id":"15414","file_name":"2024_LNCS_Avni.pdf","date_updated":"2024-05-22T07:09:24Z","relation":"main_file"}],"citation":{"ama":"Avni G, Mallik K, Sadhukhan S. Auction-based scheduling. In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:153-172. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">10.1007/978-3-031-57256-2_8</a>","apa":"Avni, G., Mallik, K., &#38; Sadhukhan, S. (2024). Auction-based scheduling. In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 153–172). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">https://doi.org/10.1007/978-3-031-57256-2_8</a>","chicago":"Avni, Guy, Kaushik Mallik, and Suman Sadhukhan. “Auction-Based Scheduling.” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:153–72. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">https://doi.org/10.1007/978-3-031-57256-2_8</a>.","ista":"Avni G, Mallik K, Sadhukhan S. 2024. Auction-based scheduling. 30th 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. 14572, 153–172.","short":"G. Avni, K. Mallik, S. Sadhukhan, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 153–172.","mla":"Avni, Guy, et al. “Auction-Based Scheduling.” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 153–72, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_8\">10.1007/978-3-031-57256-2_8</a>.","ieee":"G. Avni, K. Mallik, and S. Sadhukhan, “Auction-based scheduling,” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 153–172."},"status":"public","title":"Auction-based scheduling","corr_author":"1","quality_controlled":"1","oa_version":"Published Version","external_id":{"isi":["001284187100008"],"arxiv":["2310.11798"]},"day":"05","oa":1,"isi":1,"publisher":"Springer Nature","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","type":"conference","volume":14572,"arxiv":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"date_published":"2024-04-05T00:00:00Z","date_updated":"2025-09-08T07:33:43Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"year":"2024","month":"04"},{"has_accepted_license":"1","ddc":["000"],"date_created":"2024-05-12T22:01:02Z","author":[{"first_name":"Rupak","last_name":"Majumdar","full_name":"Majumdar, Rupak"},{"full_name":"Sağlam, Irmak","last_name":"Sağlam","first_name":"Irmak"},{"full_name":"Thejaswini, K. S.","first_name":"K. S.","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","last_name":"Thejaswini"}],"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"intvolume":"     14572","acknowledgement":"This work is a part of the project VAMOS that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, grant agreements No 101020093. Rupak Majumdar was partially supported by the DFG project 389792660 TRR 248-CPEC.","doi":"10.1007/978-3-031-57256-2_11","department":[{"_id":"ToHe"}],"scopus_import":"1","abstract":[{"text":"We provide an algorithmto solve Rabin and Streett games over graphs\r\nwith n vertices,m edges, and k colours that runs in ˜O³mn(k!)1+o(1)´time and\r\nO(nk logk logn) space, where ˜O hides poly-logarithmic factors. Our algorithm\r\nis an improvement by a super quadratic dependence on k! from the currently\r\nbest known run time of O³mn2(k!)2+o(1)´, obtained by converting a Rabin\r\ngameinto a parity game,while simultaneously improving its exponential space\r\nrequirement.\r\nOur main technical ingredient is a characterisation of progress measures for\r\nRabin games using colourful trees and a combinatorial construction of succinctlyrepresented,\r\nuniversal colourful trees. Colourful universal trees are generalisations\r\nof universal trees used by Jurdzi´nski and Lazi´c (2017) to solve parity\r\ngames, as well as of Rabin progress measures of Klarlund and Kozen (1991).\r\nOur algorithm for Rabin games is a progress measure lifting algorithm where\r\nthe lifting is performed on succinct, colourful, universal trees.","lang":"eng"}],"ec_funded":1,"file_date_updated":"2024-05-22T07:24:45Z","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031572555"]},"alternative_title":["LNCS"],"_id":"15377","article_processing_charge":"Yes (in subscription journal)","publication_status":"published","external_id":{"isi":["001284187100011"],"arxiv":["2401.07548"]},"day":"06","oa":1,"oa_version":"Published Version","quality_controlled":"1","corr_author":"1","title":"Rabin games and colourful universal trees","status":"public","file":[{"content_type":"application/pdf","checksum":"492be74f69cd6ea42d38681082d0b521","file_size":462173,"relation":"main_file","success":1,"file_id":"15415","date_updated":"2024-05-22T07:24:45Z","file_name":"2024_LNCS_Majumdar.pdf","access_level":"open_access","date_created":"2024-05-22T07:24:45Z","creator":"dernst"}],"citation":{"chicago":"Majumdar, Rupak, Irmak Sağlam, and K. S. Thejaswini. “Rabin Games and Colourful Universal Trees.” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:213–31. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">https://doi.org/10.1007/978-3-031-57256-2_11</a>.","ista":"Majumdar R, Sağlam I, Thejaswini KS. 2024. Rabin games and colourful universal trees. 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 14572, 213–231.","apa":"Majumdar, R., Sağlam, I., &#38; Thejaswini, K. S. (2024). Rabin games and colourful universal trees. In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 213–231). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">https://doi.org/10.1007/978-3-031-57256-2_11</a>","ama":"Majumdar R, Sağlam I, Thejaswini KS. Rabin games and colourful universal trees. In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:213-231. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">10.1007/978-3-031-57256-2_11</a>","ieee":"R. Majumdar, I. Sağlam, and K. S. Thejaswini, “Rabin games and colourful universal trees,” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 2024, vol. 14572, pp. 213–231.","short":"R. Majumdar, I. Sağlam, K.S. Thejaswini, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 213–231.","mla":"Majumdar, Rupak, et al. “Rabin Games and Colourful Universal Trees.” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 213–31, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_11\">10.1007/978-3-031-57256-2_11</a>."},"page":"213-231","year":"2024","month":"04","language":[{"iso":"eng"}],"date_published":"2024-04-06T00:00:00Z","date_updated":"2025-09-08T07:34:49Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"arxiv":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":14572,"type":"conference","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","publisher":"Springer Nature","isi":1}]