@inproceedings{15333,
  abstract     = {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.},
  author       = {Chalupa, Marek and Richter, Cedric},
  booktitle    = {30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031572555},
  issn         = {1611-3349},
  location     = {Luxembourg City, Luxembourg},
  pages        = {353–358},
  publisher    = {Springer Nature},
  title        = {{Bubaak-SpLit: Split what you cannot verify (Competition contribution)}},
  doi          = {10.1007/978-3-031-57256-2_20},
  volume       = {14572},
  year         = {2024},
}

@inproceedings{15376,
  abstract     = {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.},
  author       = {Avni, Guy and Mallik, Kaushik and Sadhukhan, Suman},
  booktitle    = {30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031572555},
  issn         = {1611-3349},
  location     = {Luxembourg City, Luxembourg},
  pages        = {153--172},
  publisher    = {Springer Nature},
  title        = {{Auction-based scheduling}},
  doi          = {10.1007/978-3-031-57256-2_8},
  volume       = {14572},
  year         = {2024},
}

@inproceedings{15377,
  abstract     = {We provide an algorithmto solve Rabin and Streett games over graphs
with n vertices,m edges, and k colours that runs in ˜O³mn(k!)1+o(1)´time and
O(nk logk logn) space, where ˜O hides poly-logarithmic factors. Our algorithm
is an improvement by a super quadratic dependence on k! from the currently
best known run time of O³mn2(k!)2+o(1)´, obtained by converting a Rabin
gameinto a parity game,while simultaneously improving its exponential space
requirement.
Our main technical ingredient is a characterisation of progress measures for
Rabin games using colourful trees and a combinatorial construction of succinctlyrepresented,
universal colourful trees. Colourful universal trees are generalisations
of universal trees used by Jurdzi´nski and Lazi´c (2017) to solve parity
games, as well as of Rabin progress measures of Klarlund and Kozen (1991).
Our algorithm for Rabin games is a progress measure lifting algorithm where
the lifting is performed on succinct, colourful, universal trees.},
  author       = {Majumdar, Rupak and Sağlam, Irmak and Thejaswini, K. S.},
  booktitle    = {30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031572555},
  issn         = {1611-3349},
  pages        = {213--231},
  publisher    = {Springer Nature},
  title        = {{Rabin games and colourful universal trees}},
  doi          = {10.1007/978-3-031-57256-2_11},
  volume       = {14572},
  year         = {2024},
}