3 citations · 16 across the 22 of their papers we have counts for
12 papers · 1 filter
A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions (Technical Report)
Yu-Fang Chen, Vojtěch Havlena, Ondřej Lengál +1
Case split is a core proof rule in current decision procedures for the theory of string constraints. Its use is the primary cause of the state space explosion in string constraint…
An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits (Technical Report)
Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál +3
We introduce a new paradigm for analysing and finding bugs in quantum circuits. In our approach, the problem is given by a triple and the question is whether, giv…
Word Equations in Synergy with Regular Constraints (Technical Report)
František Blahoudek, Yu-Fang Chen, David Chocholatý +4
When eating spaghetti, one should have the sauce and noodles mixed instead of eating them separately. We argue that also in string solving, word equations and regular constraints a…
Towards Efficient Matching of Regexes with Backreferences using Register Set Automata (Technical Report)
Vojtěch Havlena, Lukáš Holík, Ondřej Lengál +2
Matching regexes (regular expressions) is a common problem in many areas of computer science, with requirements on high speed and robust performance. Regexes with backreferences al…
Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation (Technical Report)
Vojtěch Havlena, Ondřej Lengál, Barbora Šmahlíková
We propose several heuristics for mitigating one of the main causes of combinatorial explosion in rank-based complementation of Büchi automata (BAs): unnecessarily high bounds on t…
Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report)
Vojtěch Havlena, Ondřej Lengál
This paper provides several optimizations of the rank-based approach for complementing Büchi automata. We start with Schewe's theoretically optimal construction and develop a set o…
Automata Terms in a Lazy WSkS Decision Procedure (Technical Report)
Vojtěch Havlena, Lukáš Holík, Ondřej Lengál +1
We propose a lazy decision procedure for the logic WSkS. It builds a term-based symbolic representation of the state space of the tree automaton (TA) constructed by the classical W…
Simulation Algorithms for Symbolic Automata (Technical Report)
Lukáš Holík, Ondřej Lengál, Juraj Síč +2
We investigate means of efficient computation of the simulation relation over symbolic finite automata (SFAs), i.e., finite automata with transitions labeled by predicates over alp…
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
Ondrej Lengal, Anthony W. Lin, Rupak Majumdar +1
We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversa…
Lazy Automata Techniques for WS1S
Tomáš Fiedor, Lukáš Holík, Petr Janků +2
We present a new decision procedure for the logic WS1S. It originates from the classical approach, which first builds an automaton accepting all models of a formula and then tests…
Nested Antichains for WS1S
Tomas Fiedor, Lukas Holik, Ondrej Lengal +1
We propose a novel approach for coping with alternating quantification as the main source of nonelementary complexity of deciding WS1S formulae. Our approach is applicable within t…
Fully Automated Shape Analysis Based on Forest Automata
Lukas Holik, Ondrej Lengal, Adam Rogalewicz +2
Forest automata (FA) have recently been proposed as a tool for shape analysis of complex heap structures. FA encode sets of tree decompositions of heap graphs in the form of tuples…