Arrow Research search

Author name cluster

Helmut Seidl

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

16 papers
2 author rows

Possible papers

16

TACAS Conference 2026 Conference Paper

Goblint: A Portfolio for Mixed Flow-Sensitive Abstract Interpretation

  • Simmo Saan
  • Ali Rasim Kocal
  • Michael Petter
  • Karoliine Holter
  • Julian Erhard
  • Michael Schwarz
  • Vesal Vojdani
  • Helmut Seidl

Abstract Goblint is a static analyzer for C programs based on abstract interpretation. It provides a flexible framework for combining analyses and specifying what information is tracked flow- and context-sensitively. For SV-COMP 2026, we adopt a sequential portfolio of configurations of increasing precision that exploits Goblint ’s rich family of abstract domains and sensitivity options. We have improved the analyses by adding bit-level and sparse affine equalities domains, new forms of path-sensitivity, and a context gas mechanism that controls context-sensitivity for recursive programs. Goblint continues its unblemished track record of sound verification across all SV-COMP benchmarks.

DOI

FM Conference 2026 Conference Paper

Mixed Flow-Sensitive Static Analysis: Engineering Modularity

  • Helmut Seidl
  • Vesal Vojdani
  • Julian Erhard
  • Michael Schwarz

Abstract Flow-sensitive and flow-insensitive analyses of programs occupy opposite ends of a spectrum. Between these extremes lie mixed flow sensitive approaches, where some aspects of program behavior are analyzed flow-insensitively and others flow-sensitively. Mixed flow-sensitivity arises, for example, in the analysis of multi-threaded code or code withnon-local control flow. Another instance is global store widening for efficient analysis of functional languages and some forms of pointer analysis. While mixed flow-sensitive analyses are common in the literature, the formulation of the particular analysis problem and the means to solve it are often tightly coupled. Side-effecting constraint systems provide a generic mechanism for describing mixed flow-sensitive analyses, thus decoupling the analysis definition from solver algorithm details. The abstract interpreter Goblint realizes this decoupling, and allows defining mixed flow-sensitive analyses independently of generic solvers. We indicate how the precision of specified analyses can be improved using digests (on the side of the formulation of the analysis problem) and suitable update rules (on the side of the solver). We explain how developers can use Goblint to implement their own mixed flow-sensitive analyses.

DOI

TACAS Conference 2026 Conference Paper

Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities

  • Ali Rasim Kocal
  • Michael Schwarz
  • Simmo Saan
  • Helmut Seidl

Abstract Fixpoint iteration constitutes the algorithmic core of static analyzers. Parallelizing the fixpoint engine can significantly reduce analysis times. Previous approaches typically fix the granularity of tasks upfront, e. g. , at the level of program threads or procedures — yielding an engine permanently stuck in one gear. Instead, we propose to parallelize a generic fixpoint engine in a way that is parametric in the task granularity — meaning that our engine can be run in different gears. We build on the top-down solver TD, extended with support for mixed-flow sensitivity, and realize two competing philosophies for parallelization, both building on a task pool that schedules tasks to a fixed number of workers. The nature of tasks differs between the philosophies. In the immediate approach, all tasks access a single thread-safe hash table maintaining solver state, while in the independent approach, each task has its own state and exchanges data with other tasks via a publish/subscribe data structure. We have equipped the fixpoint engine of the static analysis framework Goblint with implementations following both philosophies and report on our results for large real-world programs.

DOI

TCS Journal 2016 Journal Article

Look-ahead removal for total deterministic 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 before processing it. In certain cases, such a look-ahead can be avoided and the transformation can be realized by a transducer without look-ahead. Removing the look-ahead from a transducer, if possible, is technically highly challenging. For a restricted class of transducers with look-ahead, namely those that are total, deterministic, ultralinear, and bounded erasing, we present an algorithm that, for a given transducer from that class, (1) decides whether it is equivalent to a total deterministic transducer without look-ahead, and (2) constructs such a transducer if the answer is positive. For the whole class of total deterministic transducers with look-ahead we present a similar algorithm, which assumes that a so-called difference bound is known for the given transducer. The designer of a transducer can usually also determine a difference bound for it.

Details DOI

FOCS Conference 2015 Conference Paper

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 efficient algorithms for subclasses: polynomial time for total transducers with unary output alphabet (over a given top-down regular domain language), and co-randomized polynomial time for linear transducers, these results are obtained using techniques from multi-linear algebra. For our main result, we prove that equivalence can be certified by means of inductive invariants using polynomial ideals. This allows us to construct two semi-algorithms, one searching for a proof of equivalence, one for a witness of non-equivalence.

Details

CSL Conference 2007 Invited Paper

Precise Relational Invariants Through Strategy Iteration

  • Thomas Gawlitza
  • Helmut Seidl

Abstract We present a practical algorithm for computing exact least solutions of systems of equations over the rationals with addition, multiplication with positive constants, minimum and maximum. The algorithm is based on strategy improvement combined with solving linear programming problems for each selected strategy. We apply our technique to compute the abstract least fixpoint semantics of affine programs over the relational template constraint matrix domain [20]. In particular, we thus obtain practical algorithms for computing the abstract least fixpoint semantics over the zone and octagon abstract domain.

Details

LPAR Conference 2004 Conference Paper

A Generic Framework for Interprocedural Analyses of Numerical Properties

  • Markus Müller-Olm
  • Helmut Seidl

Abstract Relations among program variables like 1 + 3 · x 1 + 5 · x 2 ≡ 0 [224] have been called linear congruence relations. Such a relation is valid at a program point iff it is satisfied by all reaching program states. Knowledge about non-trivial valid congruence relations is crucial for various aggressive program transformations. It can also form the backbone of a program correctness proof. In his seminal paper [1], Philippe Granger presents an intraprocedural analysis which is able to infer linear congruence relations between integer variables. For affine programs, i. e. , programs where all assignments are affine expressions and branching is non-deterministic, Granger’s analysis is complete, i. e. , infers all valid congruence relations between variables. No upper bound, though, has been proven for Granger’s algorithm. Here, we present a variation of Granger’s analysis which runs in polynomial time. Moreover, we provide an interprocedural extension of this algorithm. The polynomial algorithm as well as its interprocedural extension are obtained by means of multiple instances of a general framework for constructing interprocedural analyses of numerical properties. This framework can be used for different numerical domains such as fields or modular rings and thus also covers the interprocedural analyses of [2, 3] where valid affine relations are inferred. We also indicate how the base technique can be extended to deal with equality guards in the interprocedural setting.

Details

LPAR Conference 2004 Conference Paper

Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying

  • Helmut Seidl
  • Kumar Neeraj Verma

Abstract Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class \(\mathcal C\) of first order clauses, which extends the Skolem class. They showed its satisfiability problem to be in 3-DEXPTIME. We improve this result by showing that satisfiability for this class is NEXPTIME-complete, using new resolution techniques. We show satisfiability to be DEXPTIME-complete if clauses are Horn, which is what is required for modeling cryptographic protocols. While translation to Horn clauses only gives a DEXPTIME upper bound for the secrecy problem for these protocols, we further show that this secrecy problem is actually DEXPTIME-complete.

Details

STOC Conference 2001 Conference Paper

On optimal slicing of parallel programs

  • Markus Müller-Olm
  • Helmut Seidl

Optimal program slicing determines for a statement S in a program π whether or not S affects a specified set of statements, given that all conditionals in π are interpreted as non-deterministic choices.

Details

CSL Conference 1999 Conference Paper

On Guarding Nested Fixpoints

  • Helmut Seidl
  • Andreas Neumann 0001

Abstract For every hierarchicalsystem of equations S over some complete and distributive lattice we construct an equivalent system with the same set of variables which additionally is guarded. The price to be paid is that the resulting right-hand sides may grow exponentially. We therefore present methods how the exponentialbl ow-up can be avoided. Especially, the loop structure of the variable dependence graph is taken into account. Also we prove that size O ( m · S ) suffices whenever S originates from a fixpoint expression where the nesting-depth of fixpoints is at most m. Finally, we sketch an application to regular tree pattern-matching.

Details

TCS Journal 1994 Journal Article

Finite tree automata with cost functions

  • Helmut Seidl

Cost functions for tree automata are mappings from transitions to (tuples of) polynomials over some semiring. We consider four semirings, namely, N the semiring of nonnegative integers, A the “arctical semiring”. T the tropical semiring and F the semiring of finite subsets of nonnegative integers. We show: for semirings N and A it is decidable in polynomial time whether or not the costs of accepting computations is bounded; for F it is decidable in polynomial time whether or not the cardinalities of occurring cost sets are bounded. In all three cases, we derive explicit upper bounds. For semiring T, we prove decidability of boundedness as well, but obtain a polynomial-time algorithm only in case that the degrees of occurring polynomials are at most 1. For N and A, we extend our results to multidimensional cost functions.

Details DOI

TCS Journal 1992 Journal Article

Single-valuedness of tree transducers is decidable in polynomial time

  • Helmut Seidl

A bottom-up finite-state tree transducer (FST) A is called single-valued iff for every input tree there is at most one output tree. We give a polynomial-time algorithm which decides whether or not a given FST is single-valued. The algorithm is based on: • the freedom of the submonoid of trees which contain at least one occurrence of one variable ∗; • the succinct representation of trees by graphs; • a sequence of normalizing transformations of the given transducer; and • a polynomially decidable characterization of pairs of equivalent output functions. We apply these methods to show that finite-valuedness is decidable in polynomial time as well.

Details DOI

TCS Journal 1991 Journal Article

On the degree of ambiguity of finite automata

  • Andreas Weber
  • Helmut Seidl

We investigate the ambiguity behavior of finite automata in connection with their inner structure. We show that the degree of ambiguity of a finitely ambiguous nondeterministic finite automaton (NFA) with n states is at most 5 n 2 ·nn. There is a simple criterion which characterizes the infinite degree of ambiguity of an NFA, and which is decidable in polynomial time. The degree of growth of the ambiguity of an NFA is computable in polynomial time. Starting from the first result, we discuss the maximal finite degree of ambiguity of an NFA with n states, and we present subclasses of NFAs where this quantity is of order 2Θ(n).

Details DOI

TCS Journal 1987 Journal Article

Parameter-reduction of higher level grammars

  • Helmut Seidl

A higher level (OI-) grammar is called terminating if for every accessible term t there is at least one terminal term which can be derived from t. A grammar is called parameter-reduced if it is terminating and has no superfluous parameters. For every grammar G of level n0 which generates at least one term we construct grammars R(G) and P(G) such that R(G) and P(G) generate the same language as G but are terminating and parameter-reduced respectively. We introduce a hierarchy of restrictions to the delection capability of the grammars which allow a gradual decrease in the complexity of the algorithms from n-iterated exponential time to polynomial time.

Details DOI

MFCS Conference 1986 Conference Paper

On the Degree of Ambiguity of Finite Automata

  • Andreas Weber
  • Helmut Seidl

Abstract We show that the degree of ambiguity of a nondeterministic finite automaton (NFA) with n states, if finite, is not greater than 2 n·log 2 n + c 1 ·n (c 1 ≅ 2. 0566). We present an algorithm which decides in polynomial time whether the degree of ambiguity of a NFA is finite or not. Additionally, the authors obtain in [14] a corresponding upper bound for the finite valuedness of a normalized finite transducer (NFT), and also a polynomial-time algorithm which decides whether the valuedness of a NFT is finite or not.

Details
v2026.09.13