24 citations · 39 across the 15 of their papers we have counts for
22 papers
When is a Bottom-Up Deterministic Tree Translation Top-Down Deterministic?
Sebastian Maneth, Helmut Seidl
We consider two natural subclasses of deterministic top-down tree-to-tree transducers, namely, linear and uniform-copying transducers. For both classes we show that it is decidable…
Checking in Polynomial Time whether or not a Regular Tree Language is Deterministic Top-Down
Sebastian Maneth, Helmut Seidl
It is well known that for a given bottom-up tree automaton it can be decided whether or not there exists deterministic top-down tree automaton that recognized the same tree languag…
Clustered Relational Thread-Modular Abstract Interpretation with Local Traces
Michael Schwarz, Simmo Saan, Helmut Seidl +2
We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables - given that they are protected by common mute…
How to decide Functionality of Compositions of Top-Down Tree Transducers
Sebastian Maneth, Helmut Seidl, Martin Vu
We prove that functionality of compositions of top-down tree transducers is decidable by reducing the problem to the functionality of one top-down tree transducer with look-ahead.
Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap
Julian Erhard, Simmo Saan, Sarah Tilscher +4
To put static program analysis at the fingertips of the software developer, we propose a framework for interactive abstract interpretation. While providing sound analysis results,…
Improving Thread-Modular Abstract Interpretation
Michael Schwarz, Simmo Saan, Helmut Seidl +3
We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants…
Definability Results for Top-Down Tree Transducers
Sebastian Maneth, Helmut Seidl, Martin Vu
We prove that for a given deterministic top-down transducer with look-ahead it is decidable whether or not its translation is definable (1)~by a linear top-down tree transducer or…
Equivalence of Linear Tree Transducers with Output in the Free Group
Raphaela Löbel, Michael Luttenberger, Helmut Seidl
We show that equivalence of deterministic linear tree transducers can be decided in polynomial time when their outputs are interpreted over the free group. Due to the cancellation…
On the Balancedness of Tree-to-word Transducers
Raphaela Löbel, Michael Luttenberger, Helmut Seidl
A language over an alphabet of opening () and closing () brackets, is balanced if it is a subset of the Dyck language over , and…
How to Win First-Order Safety Games
Helmut Seidl, Christian Müller, Bernd Finkbeiner
First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent…
Deciding Equivalence of Separated Non-Nested Attribute Systems in Polynomial Time
Helmut Seidl, Raphaela Palenta, Sebastian Maneth
In 1982, Courcelle and Franchi-Zannettacci showed that the equivalence problem of separated non-nested attribute systems can be reduced to the equivalence problem of total determin…
Verifying Security Policies in Multi-agent Workflows with Loops
Bernd Finkbeiner, Christian Müller, Helmut Seidl +1
We consider the automatic verification of information flow security policies of web-based workflows, such as conference submission systems like EasyChair. Our workflow description…
Computing the longest common prefix of a context-free language in polynomial time
Michael Luttenberger, Raphaela Palenta, Helmut Seidl
We present two structural results concerning longest common prefixes of non-empty languages. First, we show that the longest common prefix of the language generated by a context-fr…
Reachability for dynamic parametric processes
Anca Muscholl, Helmut Seidl, Igor Walukiewicz
In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables t…
Enforcing Termination of Interprocedural Analysis
Stefan Schulze Frielinghaus, Helmut Seidl, Ralf Vogler
Interprocedural analysis by means of partial tabulation of summary functions may not terminate when the same procedure is analyzed for infinitely many abstract calling contexts or…
Efficiently intertwining widening and narrowing
Gianluca Amato, Francesca Scozzari, Helmut Seidl +2
Non-trivial analysis problems require posets with infinite ascending and descending chains. In order to compute reasonably precise post-fixpoints of the resulting systems of equati…
Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable
Helmut Seidl, Sebastian Maneth, Gregor Kemper
We show that equivalence of deterministic top-down tree-to-string transducers is decidable, thus solving a long standing open problem in formal language theory. We also present eff…
Inter-procedural Two-Variable Herbrand Equalities
Stefan Schulze Frielinghaus, Michael Petter, Helmut Seidl
We prove that all valid Herbrand equalities can be inter-procedurally inferred for programs where all assignments whose right-hand sides depend on at most one variable are taken in…
Parametric Strategy Iteration
Thomas M. Gawlitza, Martin D. Schwarz, Helmut Seidl
Program behavior may depend on parameters, which are either configured before compilation time, or provided at run-time, e.g., by sensors or other input devices. Parametric program…
Look-Ahead Removal for Top-Down Tree Transducers
Joost Engelfriet, Sebastian Maneth, Helmut Seidl
Top-down tree transducers are a convenient formalism for describing tree transformations. They can be equipped with regular look-ahead, which allows them to inspect a subtree befor…
Numerical Invariants through Convex Relaxation and Max-Strategy Iteration
Thomas Martin Gawlitza, Helmut Seidl
In this article we develop a max-strategy improvement algorithm for computing least fixpoints of operators on on the reals that are point-wise maxima of finitely many monotone and…
Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying
Helmut Seidl, Kumar Neeraj Verma
Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class of first order clauses. They showed its satisfiabil…