activity
20242026
most citedString Solving with Stabilization and Transducers (Technical Report)

1 citations · 1 across the 2 of their papers we have counts for

collaborators

5 papers

cs.FL2026

Complementing Emerson-Lei Elevator Automata (Technical Report)

Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál +2

Büchi elevator automata naturally appear in several areas of formal methods as a structural expressibly-equivalent subclass of Büchi automata where every strongly connected compo…

cs.FL20261 cited

String Solving with Stabilization and Transducers (Technical Report)

David Chocholatý, Vojtěch Havlena, Lukáš Holík +2

We generalize an efficient automata-based approach to string constraint solving, the stabilization-based method behind the solver Z3-Noodler, to support relational constraints repr…

cs.LO2025

Negated String Containment is Decidable (Technical Report)

Vojtěch Havlena, Michal Hečko, Lukáš Holík +1

We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbol…

cs.LO2025

A Uniform Framework for Handling Position Constraints in String Solving (Technical Report)

Yu-Fang Chen, Vojtěch Havlena, Michal Hečko +2

We introduce a novel decision procedure for solving the class of position string constraints, which includes string disequalities, not-prefixof, not-suffixof, strat, and not-str…

cs.LO2024

Complementation of Emerson-Lei Automata (Technical Report)

Vojtěch Havlena, Ondřej Lengál, Barbora Šmahlíková

We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based Büchi automata complementation. In particular, we propose a specia…