Kontakt:

Foto von Helmut Seidl

Prof. Dr. Helmut Seidl

Forschungsschwerpunkte

  • Automatische Programmanalyse
  • Design und Implementierung von Programmiersprachen
  • Semi-strukturierte Daten
  • Baumautomaten

Veröffentlichungen

..

Deciding Equivalence of Separated Non-nested Attribute Systems in Polynomial Time.

mehr

..

Deciding Equivalence of Separated Non-Nested Attribute Systems in Polynomial Time.

mehr

..

How to Win First-Order Safety Games.

mehr

..

Enforcing termination of interprocedural analysis.

mehr

..

Balancedness of MSO transductions in polynomial time.

mehr

..

Equivalence of Deterministic Top-Down Tree-to-String Transducers Is Decidable.

mehr

..

Paths, tree homomorphisms and disequalities for -clauses.

mehr

..

Inductive Invariants for Noninterference in Multi-agent Workflows.

mehr

..

Three Improvements to the Top-Down Solver.

mehr

..

Computing the Longest Common Prefix of a Context-free Language in Polynomial Time.

mehr

..

Inter-procedural Two-Variable Herbrand Equalities.

mehr

..

Proving Absence of Starvation by Means of Abstract Interpretation and Model Checking.

mehr

..

Verifying Security Policies in Multi-agent Workflows with Loops.

mehr

..

Reachability for Dynamic Parametric Processes.

mehr

..

Computing the longest common prefix of a context-free language in polynomial time.

mehr

..

Verifying Security Policies in Multi-agent Workflows with Loops.

mehr

..

Formal Methods of Transformations (Dagstuhl Seminar 17142).

mehr

..

Efficiently intertwining widening and narrowing.

mehr

..

Look-ahead removal for total deterministic top-down tree transducers.

mehr

..

Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents.

mehr

..

Enhancing Top-Down Solving with Widening and Narrowing.

mehr

..

Static race detection for device drivers: the Goblint approach.

mehr

..

Enforcing Termination of Interprocedural Analysis.

mehr

..

Equivalence - Combinatorics, Algebra, Proofs.


..

Enforcing Termination of Interprocedural Analysis.

mehr

..

Reachability for dynamic parametric processes.

mehr

..

An Analysis of Universal Information Flow Based on Self-Composition.

mehr

..

Inter-procedural Two-Variable Herbrand Equalities.

mehr

..

Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable.

mehr

..

Transforming XML Streams with References.

mehr

..

Efficiently intertwining widening and narrowing.

mehr

..

Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable.

mehr

..

Numerical invariants through convex relaxation and max-strategy iteration.

mehr

..

How to Remove the Look-Ahead of Top-Down Tree Transducers.

mehr

..

Interprocedural Information Flow Analysis of XML Processors.

mehr

..

Parametric Strategy Iteration.

mehr

..

Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs.

mehr

..

Frameworks for Interprocedural Analysis of Concurrent Programs.

mehr

..

Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings.

mehr

..

Software Systems Safety.


..

Parametric Strategy Iteration.


..

Inter-procedural Two-Variable Herbrand Equalities.

mehr

..

Compiler Design - Syntactic and Semantic Analysis.

mehr

..

Relational abstract interpretation for the verification of 2-hypersafety properties.

mehr

..

How to combine widening and narrowing for non-monotonic systems of equations.

mehr

..

Contextual Locking for Dynamic Pushdown Networks.

mehr

..

Look-Ahead Removal for Top-Down Tree Transducers.

mehr

..

Tree Transducers and Formal Methods (Dagstuhl Seminar 13192).

mehr

..

Compiler Design - Analysis and Transformation.

mehr

..

Abstract interpretation meets convex optimization.

mehr

..

Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis.

mehr

..

Runtime Enforcement of Information Flow Security in Tree Manipulating Processes.

mehr

..

Extending ${\cal H}_1$ -Clauses with Path Disequalities.

mehr

..

Model Checking Information Flow in Reactive Systems.

mehr

..

Crossing the Syntactic Barrier: Hom-Disequalities for H1-Clauses.

mehr

..

Type Checking of Tree Walking Transducers.

mehr

..

Precise Program Analysis through Strategy Iteration and Optimization.

mehr

..

Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings.

:
Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Lecture Notes in Computer Science 7211, Springer , ISBN 978-3-642-28868-5 [contents]
mehr

..

Numerical Invariants through Convex Relaxation and Max-Strategy Iteration.

mehr

..

Earliest Normal Form and Minimization for Bottom-up Tree Transducers.

mehr

..

Extending H1-clauses with disequalities.

mehr

..

Solving systems of rational equations through strategy iteration.

mehr

..

Fast interprocedural linear two-variable equalities.

mehr

..

Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol.

mehr

..

Side-Effect Analysis of Assembly Code.

mehr

..

Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation.

mehr

..

Compiler Design - Virtual Machines.

mehr

..

Praktische Programmverifikation durch statische Analyse.

mehr

..

Interprocedural Control Flow Reconstruction.

mehr

..

Abstract Interpretation over Zones without Widening.

mehr

..

Minimization of Deterministic Bottom-Up Tree Transducers.

mehr

..

What Is a Pure Functional?

mehr

..

Bottom-Up Tree Automata with Term Constraints.

mehr

..

Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely.

mehr

..

Verifying a Local Generic Solver in Coq.

mehr

..

Normalization of Linear Horn Clauses.

mehr

..

Shape Analysis of Low-Level C with Overlapping Structures.

mehr

..

Deciding equivalence of top-down XML transformations in polynomial time.

mehr

..

Polynomial Precise Interval Analysis Revisited.


..

Games through Nested Fixpoints.

mehr

..

A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis.

mehr

..

Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case.

mehr

..

Region Analysis for Race Detection.

mehr

..

Program Analysis through Finite Tree Automata.

mehr

..

Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying.

mehr

..

Counting in trees.


..

Upper Adjoints for Fast Inter-procedural Variable Equalities.

mehr

..

Precise Interval Analysis vs. Parity Games.

mehr

..

Lightweight Verification 2008.

mehr

..

Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations.

mehr

..

Analysing All Polynomial Equations in .

mehr

..

Analysis of modular arithmetic.

mehr

..

Computing Game Values for Crash Games.

mehr

..

Precise Relational Invariants Through Strategy Iteration.

mehr

..

Interprocedurally Analysing Linear Inequality Relations.

mehr

..

Precise Fixpoint Computation Through Strategy Iteration.

mehr

..

Exact XML Type Checking in Polynomial Time.

mehr

..

Deciding Equivalence of Top-Down XML Transformations in Polynomial Time.

mehr

..

Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings.

:
Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings. Lecture Notes in Computer Science 4423, Springer , ISBN 978-3-540-71388-3 [contents]
mehr

..

Infinite-state high-level MSCs: Model-checking and realizability.

mehr

..

Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses.

mehr

..

Interprocedurally Analyzing Polynomial Identities.

mehr

..

Exact XML Type Checking in Polynomial Time.

mehr

..

On the Complexity of Equational Horn Clauses.

mehr

..

Interprocedural Herbrand Equalities.

mehr

..

Analysis of Modular Arithmetic.

mehr

..

XML type checking with macro tree transducers.

mehr

..

A Generic Framework for Interprocedural Analysis of Numerical Properties.

mehr

..

Checking Herbrand Equalities and Beyond.

mehr

..

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

mehr

..

Macro forest transducers.

mehr

..

Computing polynomial program invariants.

mehr

..

Binary Queries for Document Trees.

mehr

..

Annotiertes Lecture Recording.

mehr

..

A Note on Karr's Algorithm.

mehr

..

Counting in Trees for Free.

mehr

..

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

mehr

..

A Generic Framework for Interprocedural Analyses of Numerical Properties.

mehr

..

Precise interprocedural analysis through linear algebra.

mehr

..

The Succinct Solver Suite.


..

(Linear) Algebra for Program Analysis Dynamische Programmanalyse.

mehr

..

Numerical document queries.

mehr

..

A Succinct Solver for ALFP.

mehr

..

Transparent teleteaching.

mehr

..

Automatic Complexity Analysis.

mehr

..

Binary Queries.


..

A Type-safe Macro System for XML.

mehr

..

Infinite-State High-Level MSCs: Model-Checking and Realizability.

mehr

..

Polynomial Constants Are Decidable.

mehr

..

Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi.

mehr

..

Polynomial Constants are Decidable.

mehr

..

Interprocedural Invariants.

mehr

..

On the Expressiveness of Tree Set Operators.

, :
On the Expressiveness of Tree Set Operators. Universität Trier, Mathematik/Informatik, Forschungsbericht 02-17 ()
mehr

..

Cryptographic Analysis in Cubic Time.

mehr

..

Control-Flow Analysis in Cubic Time.

mehr

..

Synchronized Tree Languages Revisited and New Applications.

mehr

..

Weakly Regular Relations and Applications.

mehr

..

On optimal slicing of parallel programs.

mehr

..

Succinct Solvers.

mehr

..

Interprocedural Analyses: A Comparison.

mehr

..

Constraint-Based Inter-Procedural Analysis of Parallel Programs.

mehr

..

Constraint-Based Inter-Procedural Analysis of Parallel Programs.

mehr

..

On distributive fixed-point expressions.

mehr

..

A Faster Solver for General Systems of Equations.

mehr

..

On Guarding Nested Fixpoints.

mehr

..

ForkLight: A Control-Synchronous Parallel Programming Language.

mehr

..

The SPARAMAT Approach to Automatic Comprehension of Sparse Matrix Computations.

mehr

..

Propagating Differences: An Efficient New Fixpoint Algorithm for Distributive Constraint Systems.

mehr

..

Constraints to Stop Deforestation.

mehr

..

Propagating Differences: An Efficient New Fixpoint Algorithm for Distributive Constraint Systems.

mehr

..

Locating Matches of Tree Patterns in Forests.

mehr

..

Locating Matches of Tree Patterns in Forests.

, :
Locating Matches of Tree Patterns in Forests. Universität Trier, Mathematik/Informatik, Forschungsbericht 98-08 ()
mehr

..

ForkLight: A Control-Synchronous Parallel Programming Language.

, :
ForkLight: A Control-Synchronous Parallel Programming Language. Universität Trier, Mathematik/Informatik, Forschungsbericht 98-13 ()
mehr

..

The Fork95 parallel programming language: Design, implementation, application.

mehr

..

Language Support for Synchronous Parallel Critical Sections.

mehr

..

Constraints to Stop Higher-Order Deforestation.

mehr

..

Disjuntive Completion Is Not "Optimal".

mehr

..

Interprocedural Analysis Based on PDAs.

, :
Interprocedural Analysis Based on PDAs. Universität Trier, Mathematik/Informatik, Forschungsbericht 97-06 ()
mehr

..

Propagating Differences: An Efficient New Fixpoint Algorithm for Distributive Constraint Systems.

, :
Propagating Differences: An Efficient New Fixpoint Algorithm for Distributive Constraint Systems. Universität Trier, Mathematik/Informatik, Forschungsbericht 97-13 ()
mehr

..

Model-Checking for L2.

:
Model-Checking for L2. Universität Trier, Mathematik/Informatik, Forschungsbericht 97-18 ()
mehr

..

Fast and Simple Nested Fixpoints.

mehr

..

Least and Greatest Solutions of Equations over N.

mehr

..

Integer Constraints to Stop Deforestation.

mehr

..

A Modal Mu-Calculus for Durational Transition Systems.

mehr

..

An Even Faster Solver for General Systems of Equations.

mehr

..

Fast and Simple Nested Fixpoints.

:
Fast and Simple Nested Fixpoints. Universität Trier, Mathematik/Informatik, Forschungsbericht 96-05 ()
mehr

..

An Even Faster Solver for General Systems of Equations.

, :
An Even Faster Solver for General Systems of Equations. Universität Trier, Mathematik/Informatik, Forschungsbericht 96-11 ()
mehr

..

Integrating Synchronous and Asynchronous Paradigms: The Fork95 Parallel Programming Language.

, :
Integrating Synchronous and Asynchronous Paradigms: The Fork95 Parallel Programming Language. Universität Trier, Mathematik/Informatik, Forschungsbericht 95-05 ()
mehr

..

A Modal µ-Calculus for Durational Transition Systems.

:
A Modal µ-Calculus for Durational Transition Systems. Universität Trier, Mathematik/Informatik, Forschungsbericht 95-08 ()
mehr

..

Language Support for Synchronous Parallel Critical Sections.

, :
Language Support for Synchronous Parallel Critical Sections. Universität Trier, Mathematik/Informatik, Forschungsbericht 95-23 ()
mehr

..

Tree Automata for Code Selection.

mehr

..

Haskell Overloading is DEXPTIME-Complete.

mehr

..

Equivalence of Finite-Valued Tree Transducers Is Decidable.

mehr

..

Finite Tree Automata with Cost Functions.

mehr

..

Least Solutions of Equations over N.

mehr

..

When Is a Functional Tree Transduction Deterministic?

mehr

..

FORK: A high-level language for PRAMs.

mehr

..

Single-Valuedness of Tree Transducers is Decidable in Polynomial Time.

mehr

..

Finite Tree Automata with Cost Functions.

mehr

..

Ambiguity and valuedness.

mehr

..

Baumautomaten zur Codeselektion.

mehr

..

On finitely generated monoids of matrices with entries in N.

mehr

..

On the Degree of Ambiguity of Finite Automata.

mehr

..

Tree Automata for Code Selection.

mehr

..

FORK: A High-Level Language for PRAMs.

mehr

..

Deciding Equivalence of Finite Tree Automata.

mehr

..

Equivalence of Finite-Valued Bottom-up Finite State Tree Transducers Is Decidable.

:
Equivalence of Finite-Valued Bottom-up Finite State Tree Transducers Is Decidable. CAAP : 269-284
mehr

..

Characterizing Complexity Classes by Higher Type Primitive Recursive Definitions, Part II.

mehr

..

On the Finite Degree of Ambiguity of Finite Tree Automata.

mehr

..

On the Finite Degree of Ambiguity of Finite Tree Automata.

mehr

..

Deciding Equivalence of Finite Tree Automata.

mehr

..

Parameter-Reduction of Higher Level Grammars (Extended Abstract).

mehr

..

Parameter Reduction of Higher Level Grammars.

mehr

..

On the Degree of Ambiguity of Finite Automata.

mehr

..

A quadratic regularity test for non-deleting macro S grammars.

mehr