Verification and Analysis for Safety and Security of Applications in Life
Publications
Melani, B., Bartocci, E., & Chiari, M. (2025). A tree-shaped tableau for checking the satisfiability of signal temporal logic with bounded temporal operators. ACM Transactions on Embedded Computing Systems. Advance online publication. https://doi.org/10.1145/3759917
Dacík, T., & Vojnar, T. (2025). RacerF: Lightweight static data race detection for C code (Experience paper). In Proceedings of the 39th European Conference on Object-Oriented Programming (ECOOP 2025) (Leibniz International Proceedings in Informatics—LIPIcs). https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.37 This paper introduces RacerF, a lightweight static analyser for detecting data races in C programs. Built as a plugin for Frama-C, it combines under- and over-approximating methods to generalise sequential analysis to multi-threaded code. While heuristic, RacerF achieves competitive precision compared to heavyweight tools and offers faster performance in experiments.
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. https://link.springer.com/chapter/10.1007/978-3-031-98679-6_8 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.
