Verification and Analysis for Safety and Security of Applications in Life
Publications
2026
Brablec, T., Dacík, T., & Vojnar, T. SEAL: Symbolic Execution with Separation Logic (Competition Contribution). In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2026. https://link.springer.com/chapter/10.1007/978-3-032-22749-2_34 SEAL is a static analyser for the verification of programs that manipulate unbounded linked data structures. It is based on separation logic to represent abstract memory states and, unlike other separation-logic-based approaches, it employs a general-purpose separation logic solver ASTRAL for satisfiability and entailment checking, which itself is based on translation to SMT. This design results in a modular architecture intended to be easier to extend and to combine with reasoning in other theories.
Wendland, J., Zubia, M., Andriushchenko, R., Galesloot, M., Češka, M., von Kleist, H., Simão, T. D., Weininger, M., & Jansen, N. Missingness-MDPs: Bridging the Theory of Missing Data and POMDPs. In: International Joint Conference on Artificial Intelligence (IJCAI) 2026. https://arxiv.org/abs/2605.12262 This paper introduces missingness-MDPs (miss-MDPs), a novel subclass of POMDPs that integrates missing data theory to model state feature unobservability. By leveraging the structural properties of different missingness types (MCAR, MAR, MNAR), we derive PAC algorithms to learn the unknown missingness function from trajectory data and compute provably ε-optimal policies for complex partially observable environments.CORE A*
Vašíček, O., Arias, J., Fiedor, J., Gupta, G., Křena, B., Němec, J., Romero, J., & Vojnar, T. (2026). Event Calculus Meets Hybrid ASP. Theory and Practice of Logic Programming (Accepted at International Conference on Logic Programming 2026). https://www.cambridge.org/core/journals/theory-and-practice-of-logic-programming/article/event-calculus-meets-hybrid-asp/5F24373721426F75AD9CB3D1DD451BC8 This paper introduces Hybrid Event Calculus (EC), an extended axiomatization of Discrete EC that addresses the scalability and accuracy issues of existing ASP solvers when handling continuous change and large value domains. By employing functional fluents and abstract time steps alongside hybrid ASP systems (clingcon and clingo-lpx), the approach delegates dense time and system property domains to linear constraint solvers, enabling accurate, termination-guaranteed modeling of continuous systems without suffering from combinatorial explosion.Decile D1
Heck, L., Macák, F., Andriushchenko, R., Češka, M., & Junges, S. Shields to Guarantee Probabilistic Safety in MDPs. In: International Conference on Computer Aided Verification (CAV) 2026. https://arxiv.org/abs/2605.10888 https://link.springer.com/chapter/10.1007/978-3-032-32526-6_27 This paper presents a formal framework extending classical shielding to ensure probabilistic safety in autonomous agents where hazardous events are acceptable within a defined probability bound. After proving the impossibility of simultaneously preserving strong safety and maximal permissiveness in probabilistic settings, the authors establish alternative shield constructions with formal guarantees and demonstrate their practical efficacy and computational feasibility.CORE A*
Češka, M., Junges, S., van der Maas, L., Macák, F., & Quatmann, T. Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families. In: International Conference on Computer Aided Verification (CAV) 2026. https://arxiv.org/abs/2605.11897 https://link.springer.com/chapter/10.1007/978-3-032-32537-2_25 This paper presents a numerically stable, practically efficient method for computing optimal conditional reachability probabilities in Markov decision processes (MDPs) without relying on traditional cyclic reductions. The proposed approach decides the threshold problem in linear time on acyclic MDPs, scales to millions of Markov chains via abstraction-refinement, and achieves speed-ups of up to multiple orders of magnitude across benchmarks in Bayesian networks, probabilistic programs, and runtime monitoring.CORE A*
Havlena, V., Holík L., Lengál, O., Vašák, J., Gulčíková, S. Towards Efficient Matching of Regexes with Backreferences using Register Set Automata In: Conference on Programming Language Design and Implementation (PLDI) 2026. https://arxiv.org/abs/2205.12114 https://doi.org/10.1145/3808281 This paper proposes a new formal model for data word languages called Register Set Automata (RSAs), which can be seen as an extension of standard Register Automata (RAs) with the difference that registers can now hold sets of values instead of singletons. The paper establishes theoretical foundations for the model and also shows its usefulness in matching regular expressions with backreferences. For this, a determinization algorithm from RAs to deterministic RSAs is proposed. Our evaluation shows that the new formal model can give more robust matching times for a practically relevant class of regular expressions with backreferences than other state of the art matchers.CORE A*
Heck, L., Macák, F., Češka, M., & Junges, S. Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking. In: AAAI Conference on Artificial Intelligence (AAAI) 2026. https://arxiv.org/abs/2511.08078 https://doi.org/10.1609/aaai.v40i43.40944 This paper presents a novel framework for synthesizing robust and constrained policies for finite Markov decision processes (MDPs). It introduces a flexible approach that tightly integrates satisfiability solvers with probabilistic model checking to handle structural constraints and robustness across perturbations in MDPs. The method allows expressing arbitrary constraints in first-order logic over sets of MDPs and demonstrates competitive performance on benchmark problems, offering a practical solution to compute policies that satisfy both robustness and structural requirements.CORE A*
Hudák, D., Galesloot, M. F. L., Tappler, M., Kurečka, M., Jansen, N., & Češka, M. Finite-State Controllers for (Hidden-Model) POMDPs using Deep Reinforcement Learning. In: International Conference on Autonomous Agents and Multiagent Systems (AAMAS) 2026. https://arxiv.org/abs/2602.08734 https://doi.org/10.65109/TBFQ5922 This paper proposes the Lexpop framework to address planning in partially observable Markov decision processes (POMDPs) by combining deep reinforcement learning with finite-state controller (FSC) extraction. The approach trains a neural policy using recurrent architectures and then derives an interpretable FSC that can be formally verified, providing performance guarantees. It further extends the method to robustly handle hidden-model POMDPs (HM-POMDPs)—sets of related POMDPs—by iteratively refining policies against worst-case models, demonstrating improved scalability and effectiveness over existing solvers.CORE A*
2025
Hána, M., Kosmatov, N., Prevosto, V., & Signoles, J. Automated Context-Sensitive Static Analysis for Specification-Driven C Programs. In: Integrated Formal Methods: 20th International Conference (iFM) 2025. https://dl.acm.org/doi/10.1007/978-3-032-10794-7_17 This paper presents a context-sensitive static analysis framework tailored for specification-driven C programs. By integrating formal specifications into the static analysis process, the approach enhances precision and scalability when verifying program properties. It systematically combines context abstraction with specification semantics to reduce false positives while maintaining soundness, and demonstrates effectiveness on real-world codebases with rich formal specifications.
Pluska, A., & Malhotra, S. On Local Limits of Sparse Random Graphs: Color Convergence and the Refined Configuration Model. In: Conference on Neural Information Processing Systems (NeurIPS) 2025. https://doi.org/10.48550/arXiv.2510.21392 https://neurips.cc/virtual/2025/loc/san-diego/poster/116124 This paper introduces color convergence, a new notion of local convergence for sparse random graphs grounded in the Weisfeiler–Leman algorithm. Color convergence precisely characterizes random graph families that behave well as limits for message-passing graph neural networks. Building on this, the authors propose the Refined Configuration Model (RCM), a generalization of the classical configuration model. RCM is shown to be universal with respect to local convergence for locally tree-like random graph models such as Erdős–Rényi, stochastic block models, and configuration models. The framework also yields a complete characterization of the random trees that can arise as local limits of such graph families.CORE A*
Bozga, M., Iosif, R., & Zuleger, F. Regular Grammars for Sets of Graphs of Tree-Width 2. In: 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2025. https://arxiv.org/abs/2408.01226 https://doi.org/10.1109/LICS65433.2025.00059 This paper extends the concept of regular grammars from strings to graphs with bounded tree-width (up to 2), introducing regular grammars for unordered unranked trees and such graphs. It proves that these grammars precisely characterize CMSO-definable (recognizable) graph languages and establishes complexity bounds for language inclusion problems. The work bridges formal language theory and graph theory, offering a foundational framework for reasoning about graph structures through grammar-based methods.CORE A*
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. https://doi.org/10.1145/3759917 This article introduces a novel tree-shaped, one-pass tableau method for satisfiability checking of discrete-time STL with bounded temporal operators. Our tableau exploits redundancy arising from large time intervals in STL formulas to speed up satisfiability checking, and can also be employed to check Mission-Time Linear Temporal Logic (MLTL) satisfiability. The experiments show that, in many cases, our tableau outperforms state-of-the-art encodings.Quantile Q2
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) 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.CORE A
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. https://doi.org/10.24963/ijcai.2025/947 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* Best Student Paper Award
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.
