1 citations · 4 across the 10 of their papers we have counts for
10 papers
A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
Wei-Lun Tsai, Yu-Fang Chen, Ondřej Lengál
Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification…
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…
Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report)
Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen +5
We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs).…
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 special…
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)
Peter Habermehl, Vojtěch Havlena, Michal Hečko +2
We present a new angle on solving quantified linear integer arithmetic based on combining the automata-based approach, where numbers are understood as bitvectors, with ideas from (…
Z3-Noodler: An Automata-based String Solver (Technical Report)
Yu-Fang Chen, David Chocholatý, Vojtěch Havlena +3
Z3-Noodler is a fork of Z3 that replaces its string theory solver with a custom solver implementing the recently introduced stabilization-based algorithm for solving word equations…
Mata, a Fast and Simple Finite Automata Library (Technical Report)
David Chocholatý, Tomáš Fiedor, Vojtěch Havlena +4
Mata is a well-engineered automata library written in C++ that offers a unique combination of speed and simplicity. It is meant to serve in applications such as string constraint s…