---
_id: '15333'
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.
acknowledgement: This work was partially supported by the ERC-2020-AdG 10102009 grant.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Marek
  full_name: Chalupa, Marek
  id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
  last_name: Chalupa
- first_name: Cedric
  full_name: Richter, Cedric
  last_name: Richter
citation:
  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>'
  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>.'
  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.'
  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.'
  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.
conference:
  end_date: 2024-04-11
  location: Luxembourg City, Luxembourg
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2024-04-06
corr_author: '1'
date_created: 2024-04-20T18:14:06Z
date_published: 2024-04-05T00:00:00Z
date_updated: 2025-09-04T13:48:25Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_20
ec_funded: 1
external_id:
  isi:
  - '001284187100020'
file:
- access_level: open_access
  checksum: 208c855c60824bec936b8d01d0396474
  content_type: application/pdf
  creator: cchlebak
  date_created: 2024-04-26T11:27:26Z
  date_updated: 2024-04-26T11:27:26Z
  file_id: '15347'
  file_name: 2024_LNCS_Chalupa.pdf
  file_size: 577128
  relation: main_file
  success: 1
file_date_updated: 2024-04-26T11:27:26Z
has_accepted_license: '1'
intvolume: '     14572'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '04'
oa: 1
oa_version: Published Version
page: 353–358
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
  and Analysis of Systems
publication_identifier:
  eisbn:
  - '9783031572562'
  eissn:
  - 1611-3349
  isbn:
  - '9783031572555'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Bubaak-SpLit: Split what you cannot verify (Competition contribution)'
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...
---
_id: '15376'
abstract:
- lang: eng
  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.
acknowledgement: This work was supported in part by the ERC project ERC-2020-AdG 101020093
  and by ISF grant no. 1679/21.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Guy
  full_name: Avni, Guy
  id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
  last_name: Avni
  orcid: 0000-0001-5588-8287
- first_name: Kaushik
  full_name: Mallik, Kaushik
  id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
  last_name: Mallik
  orcid: 0000-0001-9864-7475
- first_name: Suman
  full_name: Sadhukhan, Suman
  last_name: Sadhukhan
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>.
  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.
  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.'
  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>.
  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.
conference:
  end_date: 2024-04-11
  location: Luxembourg City, Luxembourg
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2024-04-06
corr_author: '1'
date_created: 2024-05-12T22:01:02Z
date_published: 2024-04-05T00:00:00Z
date_updated: 2025-09-08T07:33:43Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_8
ec_funded: 1
external_id:
  arxiv:
  - '2310.11798'
  isi:
  - '001284187100008'
file:
- access_level: open_access
  checksum: dbeb123510997886d11925aedbf9c400
  content_type: application/pdf
  creator: dernst
  date_created: 2024-05-22T07:09:24Z
  date_updated: 2024-05-22T07:09:24Z
  file_id: '15414'
  file_name: 2024_LNCS_Avni.pdf
  file_size: 508191
  relation: main_file
  success: 1
file_date_updated: 2024-05-22T07:09:24Z
has_accepted_license: '1'
intvolume: '     14572'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 153-172
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
  and Analysis of Systems
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031572555'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Auction-based scheduling
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...
---
_id: '15377'
abstract:
- lang: eng
  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."
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.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Rupak
  full_name: Majumdar, Rupak
  last_name: Majumdar
- first_name: Irmak
  full_name: Sağlam, Irmak
  last_name: Sağlam
- first_name: K. S.
  full_name: Thejaswini, K. S.
  id: 3807fb92-fdc1-11ee-bb4a-b4d8a431c753
  last_name: Thejaswini
citation:
  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>'
  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>
  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>.
  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.
  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.
  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>.
  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.
corr_author: '1'
date_created: 2024-05-12T22:01:02Z
date_published: 2024-04-06T00:00:00Z
date_updated: 2025-09-08T07:34:49Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-57256-2_11
ec_funded: 1
external_id:
  arxiv:
  - '2401.07548'
  isi:
  - '001284187100011'
file:
- access_level: open_access
  checksum: 492be74f69cd6ea42d38681082d0b521
  content_type: application/pdf
  creator: dernst
  date_created: 2024-05-22T07:24:45Z
  date_updated: 2024-05-22T07:24:45Z
  file_id: '15415'
  file_name: 2024_LNCS_Majumdar.pdf
  file_size: 462173
  relation: main_file
  success: 1
file_date_updated: 2024-05-22T07:24:45Z
has_accepted_license: '1'
intvolume: '     14572'
isi: 1
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: 213-231
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 30th International Conference on Tools and Algorithms for the Construction
  and Analysis of Systems
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031572555'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Rabin games and colourful universal trees
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14572
year: '2024'
...