6 papers
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…
Parameterized Verification of Quantum Circuits (Technical Report)
Parosh Aziz Abdulla, Yu-Fang Chen, Michal HeÄko +4
We present the first fully automatic framework for verifying relational properties of parameterized quantum programs, i.e., a program that, given an input size, generates a corresp…
On Complementation of Nondeterministic Finite Automata without Full Determinization (Technical Report)
Lukáš HolÃk, OndÅej Lengál, Juraj Major +2
Complementation of finite automata is a basic operation used in numerous applications. The standard way to complement a nondeterministic finite automaton (NFA) is to transform it i…
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…
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…
Automata Size Reduction by Procedure Finding
Michal Å edý, Lukáš HolÃk
We introduce a novel paradigm for reducing the size of finite automata by compressing repeating sub-graphs. These repeating sub-graphs can be viewed as invocations of a single proc…