39 citations · 57 across the 13 of their papers we have counts for
14 papers
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…
Fast Computation of Strong Control Dependencies
Marek Chalupa, David Klaška, Jan Strejček +1
We introduce new algorithms for computing non-termination sensitive control dependence (NTSCD) and decisive order dependence (DOD). These relations on control flow graph vertices h…
LTL to Smaller Self-Loop Alternating Automata and Back
František Blahoudek, Juraj Major, Jan Strejček
Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. Th…
SBT-instrumentation: A Tool for Configurable Instrumentation of LLVM Bitcode
Martina Vitovská, Marek Chalupa, Jan Strejček
The paper describes a member of the Symbiotic toolbox called sbt-instrumentation, which is a tool for configurable instrumentation of LLVM bitcode. The tool enables a user to speci…
On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding
Martin Jonáš, Jan Strejček
We study the precise computational complexity of deciding satisfiability of first-order quantified formulas over the theory of fixed-size bit-vectors with binary-encoded bit-widths…
Tighter Loop Bound Analysis (Technical report)
Pavel Čadek, Jan Strejček, Marek Trtík
We present a new algorithm for computing upper bounds on the number of executions of each program instruction during any single program run. The upper bounds are expressed as funct…