Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. - Peter Habermehl; Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (CAV (1), 2024)

Negated String Containment Is Decidable. - Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (MFCS, 2025)

A Uniform Framework for Handling Position Constraints in String Solving. - Yu-Fang Chen 001; Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (Proc. ACM Program. Lang., 2025)

A Uniform Framework for Handling Position Constraints in String Solving (Technical Report). - Yu-Fang Chen 001; Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (CoRR, 2025)

Negated String Containment is Decidable (Technical Report). - Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (CoRR, 2025)