Martin Jonáš

TACAS Conference 2026 Conference Paper

BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability

• Jakub Horák
• Martin Jonáš

TACAS Conference 2026 Conference Paper

Re3ver: Reverse and Verify

• Adéla Štěpková
• Martin Jonáš
• Jan Strejček

TACAS Conference 2026 Conference Paper

Symbiotic 11 Predicate Abstraction Joins the Party

• Paulína Ayaziová
• Martin Jonáš
• Vincent Mihalkovič
• Jindřich Sedláček
• Jan Strejček

IJCAI Conference 2025 Conference Paper

Steady-State Strategy Synthesis for Swarms of Autonomous Agents

• Martin Jonáš
• Antonín Kučera
• Vojtěch Kůr
• Jan Mačák

The steady-state synthesis aims to construct a policy for a given MDP D such that the long-run average frequencies of visits to the vertices of D satisfy given numerical constraints. This problem is solvable in polynomial time, and memoryless policies are sufficient for approximating an arbitrary frequency vector achievable by a general (infinite-memory) policy. We study the steady-state synthesis problem for multiagent systems, where multiple autonomous agents jointly strive to achieve a suitable frequency vector. We show that the problem for multiple agents is computationally hard (PSPACE or NP hard, depending on the variant), and memoryless strategy profiles are insufficient for approximating achievable frequency vectors. Furthermore, we prove that even evaluating the frequency vector achieved by a given memoryless profile is computationally hard. This reveals a severe barrier to constructing an efficient synthesis algorithm, even for memoryless profiles. Nevertheless, we design an efficient and scalable synthesis algorithm for a subclass of full memoryless profiles, and we evaluate this algorithm on a large class of randomly generated instances. The experimental results demonstrate a significant improvement against a naive algorithm based on strategy sharing.

TCS Journal 2024 Journal Article

Truncating abstraction of bit-vector operations for BDD-based SMT solvers

• Martin Jonáš
• Jan Strejček

During the last few years, BDD-based SMT solvers proved to be competitive in deciding satisfiability of quantified bit-vector formulas. However, these solvers usually do not perform well on input formulas with complicated arithmetic. Hitherto, this problem has been alleviated by approximations reducing effective bit-widths of bit-vector variables. In this paper, we propose an orthogonal abstraction technique that works on the level of the individual instances of bit-vector operations. In particular, we compute only several bits of the operation result, which may be sufficient to decide the satisfiability of the formula. Experimental results show that our BDD-based SMT solver Q3B extended with these abstractions can solve more quantified bit-vector formulas from the smt-lib repository than SMT solvers Boolector, CVC4, and Z3.