@inproceedings{13141,
  abstract     = {We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an ω-regular winning condition Φ for the system player, we compute an ω-regular assumption Ψ for the environment player, such that (i) every environment strategy compliant with Ψ allows the system to fulfill Φ (sufficiency), (ii) Ψ
 can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness).
For parity games, which are canonical representations of ω-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for ω
-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.},
  author       = {Anand, Ashwani and Mallik, Kaushik and Nayak, Satya Prakash and Schmuck, Anne Kathrin},
  booktitle    = {TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031308192},
  issn         = {1611-3349},
  location     = {Paris, France},
  pages        = {211--228},
  publisher    = {Springer Nature},
  title        = {{Computing adequately permissive assumptions for synthesis}},
  doi          = {10.1007/978-3-031-30820-8_15},
  volume       = {13994},
  year         = {2023},
}

@inproceedings{12854,
  abstract     = {The main idea behind BUBAAK is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.
At SV-COMP  2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why BUBAAK only ran several analyses in parallel, without any coordination. Still, BUBAAK won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.},
  author       = {Chalupa, Marek and Henzinger, Thomas A},
  booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031308192},
  issn         = {1611-3349},
  location     = {Paris, France},
  pages        = {535--540},
  publisher    = {Springer Nature},
  title        = {{Bubaak: Runtime monitoring of program verifiers}},
  doi          = {10.1007/978-3-031-30820-8_32},
  volume       = {13994},
  year         = {2023},
}