Publications

• Andriushchenko R., Češka M., Junges S., Macák F. Small Decision Trees for MDPs with Deductive Synthesis. In: International Conference on Computer Aided Verification (CAV) 2025.
  This paper presents a novel algorithm for synthesizing explainable strategies in Markov decision processes represented via small decision trees. The experiments show this novel approach beats state-of-the-art by orders of magnitude. CORE A*
• Galesloot, M.F.L., Andriushchenko, R., Češka M., Junges, S., Jansen, N. rfPG: Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs. In: International Joint Conference on Artificial Intelligence (IJCAI) 2025.
  The paper introduces an approach for computing robust policies in Hidden-model POMDPs (HM-POMDPs), where the true environment model is unknown at execution time. The approach combines formal verification to identify worst-case models with gradient ascent for policy optimization. Empirical results demonstrate that the method yields more robust policies with better generalization to unseen models and scales to HM-POMDPs with over a hundred thousand environments. CORE A*
• Sextl F., Rogalewicz A., Vojnar T., Zuleger F. Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. In: European Symposium on Programming (ESOP) 2025.
  https://link.springer.com/chapter/10.1007/978-3-031-91121-7_10
  This paper presents two improvements of abduction-based compositional analysis of list-manipulating programs – shared abduction for better handling of branching and shape extrapolation for improved analysis of loops. Those techniques are shown to improve both efficiency and precision of the analysis. CORE A
• Pontiggia F., Macák F., Andriushchenko R., Chiari M., Češka M. Decentralized Planning Using Probabilistic Hyperproperties. In: International Conference on Autonomous Agents and Multiagent Systems (AAMAS) 2025.
  https://www.ifaamas.org/Proceedings/aamas2025/pdfs/p1688.pdf
  This paper proposes a new logic PHyperLTL and showcases its close relation to decentralized planning. Exploiting this relation, the authors implemented an algorithm that is able to solve interesting decentralized planning problems. CORE A*
• Chocholatý D., Havlena V., Holík L., Hranička J., Lengál O., Síč J. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2025.
  https://link.springer.com/chapter/10.1007/978-3-031-90653-4_2
  The paper describes the latest improvements in the Z3-Noodler string solver, focusing on a technique for combining several decision procedures together. CORE A
• Dacík T., Vojnar T. RacerF: Data Race Detection with Frama-C (Competition Contribution). In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2025.
  https://link.springer.com/chapter/10.1007/978-3-031-90660-2_20
  RacerF is a static analyser for detection of data races in multithreaded C programs implemented as a plugin of the Frama-C platform. The approach behind RacerF is mostly heuristic and relies on analysis of the sequential behaviour of particular threads whose results are generalised using a combination of under- and over-approximating techniques to allow analysis of the multithreading behaviour. In particular, in SV-COMP’25, RacerF relies on the Frama-C’s abstract interpreter EVA to perform the analysis of the sequential behaviour. Although RacerF does not provide any formal guarantees, it ranked second in the NoDataRace-Main sub-category, providing the largest number of correct results (when excluding metaverifiers) and just 4 false positives.