| 2026 | ESOP | Max-Policy Iteration, Revisited. | David Monniaux, Helmut Seidl |
| 2026 | FM | Mixed Flow-Sensitive Static Analysis: Engineering Modularity. | Helmut Seidl, Vesal Vojdani, Julian Erhard, Michael Schwarz |
| 2026 | TACAS | Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities. | Ali Rasim Kocal, Michael Schwarz, Simmo Saan, Helmut Seidl |
| 2026 | TACAS | Goblint: A Portfolio for Mixed Flow-Sensitive Abstract Interpretation - (Competition Contribution). | Simmo Saan, Ali Rasim Kocal, Michael Petter, Karoliine Holter, Julian Erhard, Michael Schwarz, Vesal Vojdani, Helmut Seidl |
| 2025 | ICCS | Dead Gate Elimination. | Yanbin Chen, Christian B. Mendl, Helmut Seidl |
| 2025 | VMCAI | Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts. | Julian Erhard, Manuel Bentele, Matthias Heizmann, Dominik Klumpp, Simmo Saan, Frank Schssele, Michael Schwarz, Helmut Seidl, Sarah Tilscher, Vesal Vojdani |
| 2024 | CAV | The Top-Down Solver Verified: Building Confidence in Static Analyzers. | Yannick Stade, Sarah Tilscher, Helmut Seidl |
| 2024 | TACAS | Goblint Validator: Correctness Witness Validation by Abstract Interpretation - (Competition Contribution). | Simmo Saan, Julian Erhard, Michael Schwarz, Stanimir Bozhilov, Karoliine Holter, Sarah Tilscher, Vesal Vojdani, Helmut Seidl |
| 2024 | TACAS | Goblint: Abstract Interpretation for Memory Safety and Termination - (Competition Contribution). | Simmo Saan, Julian Erhard, Michael Schwarz, Stanimir Bozhilov, Karoliine Holter, Sarah Tilscher, Vesal Vojdani, Helmut Seidl |
| 2024 | VMCAI | Correctness Witness Validation by Abstract Interpretation. | Simmo Saan, Michael Schwarz, Julian Erhard, Helmut Seidl, Sarah Tilscher, Vesal Vojdani |
| 2023 | ESOP | Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. | Michael Schwarz, Simmo Saan, Helmut Seidl, Julian Erhard, Vesal Vojdani |
| 2023 | PLDI | When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-local Jumps in C. | Michael Schwarz, Julian Erhard, Vesal Vojdani, Simmo Saan, Helmut Seidl |
| 2023 | SAS | Octagons Revisited - Elegant Proofs and Simplified Algorithms. | Michael Schwarz, Helmut Seidl |
| 2023 | TACAS | Goblint: Autotuning Thread-Modular Abstract Interpretation - (Competition Contribution). | Simmo Saan, Michael Schwarz, Julian Erhard, Manuel Pietsch, Helmut Seidl, Sarah Tilscher, Vesal Vojdani |
| 2021 | DLT | Definability Results for Top-Down Tree Transducers. | Sebastian Maneth, Helmut Seidl, Martin Vu |
| 2021 | SAS | Improving Thread-Modular Abstract Interpretation. | Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani |
| 2021 | TACAS | Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints - (Competition Contribution). | Simmo Saan, Michael Schwarz, Kalmer Apinis, Julian Erhard, Helmut Seidl, Ralf Vogler, Vesal Vojdani |
| 2020 | DLT | Equivalence of Linear Tree Transducers with Output in the Free Group. | Raphaela Lbel, Michael Luttenberger, Helmut Seidl |
| 2020 | DLT | On the Balancedness of Tree-to-Word Transducers. | Raphaela Lbel, Michael Luttenberger, Helmut Seidl |
| 2020 | ICALP | When Is a Bottom-Up Deterministic Tree Translation Top-Down Deterministic? | Sebastian Maneth, Helmut Seidl |
| 2020 | SAS | Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis. | Anastasiia Izycheva, Eva Darulova, Helmut Seidl |
| 2020 | SAS | Stratified Guarded First-Order Transition Systems. | Christan Mller, Helmut Seidl |
| 2020 | VMCAI | How to Win First-Order Safety Games. | Helmut Seidl, Christian Mller, Bernd Finkbeiner |
| 2019 | ATVA | Synthesizing Efficient Low-Precision Kernels. | Anastasiia Izycheva, Eva Darulova, Helmut Seidl |
| 2019 | FOSSACS | Deciding Equivalence of Separated Non-nested Attribute Systems in Polynomial Time. | Helmut Seidl, Raphaela Palenta, Sebastian Maneth |
| 2018 | PPDP | Three Improvements to the Top-Down Solver. | Helmut Seidl, Ralf Vogler |
| 2018 | STACS | Computing the Longest Common Prefix of a Context-free Language in Polynomial Time. | Michael Luttenberger, Raphaela Palenta, Helmut Seidl |
| 2017 | ATVA | Proving Absence of Starvation by Means of Abstract Interpretation and Model Checking. | Helmut Seidl, Ralf Vogler |
| 2017 | CCS | Verifying Security Policies in Multi-agent Workflows with Loops. | Bernd Finkbeiner, Christian Mller, Helmut Seidl, Eugen Zalinescu |
| 2017 | VMCAI | Reachability for Dynamic Parametric Processes. | Anca Muscholl, Helmut Seidl, Igor Walukiewicz |
| 2016 | ATVA | Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents. | Bernd Finkbeiner, Helmut Seidl, Christian Mller |
| 2016 | SAS | Enforcing Termination of Interprocedural Analysis. | Stefan Schulze Frielinghaus, Helmut Seidl, Ralf Vogler |
| 2015 | ESOP | Inter-procedural Two-Variable Herbrand Equalities. | Stefan Schulze Frielinghaus, Michael Petter, Helmut Seidl |
| 2015 | FOCS | Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable. | Helmut Seidl, Sebastian Maneth, Gregor Kemper |
| 2015 | SPIRE | Transforming XML Streams with References. | Sebastian Maneth, Alberto Ordez Pereira, Helmut Seidl |
| 2014 | DLT | How to Remove the Look-Ahead of Top-Down Tree Transducers. | Joost Engelfriet, Sebastian Maneth, Helmut Seidl |
| 2014 | LATA | Interprocedural Information Flow Analysis of XML Processors. | Helmut Seidl, Mt Kovcs |
| 2014 | VMCAI | Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs. | Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Kalmer Apinis |
| 2013 | CCS | Relational abstract interpretation for the verification of 2-hypersafety properties. | Mt Kovcs, Helmut Seidl, Bernd Finkbeiner |
| 2013 | PLDI | How to combine widening and narrowing for non-monotonic systems of equations. | Kalmer Apinis, Helmut Seidl, Vesal Vojdani |
| 2013 | SAS | Contextual Locking for Dynamic Pushdown Networks. | Peter Lammich, Markus Mller-Olm, Helmut Seidl, Alexander Wenner |
| 2012 | APLAS | Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis. | Kalmer Apinis, Helmut Seidl, Vesal Vojdani |
| 2012 | FOSSACS | Extending ${\cal H}_1$ -Clauses with Path Disequalities. | Helmut Seidl, Andreas Reu |
| 2012 | VMCAI | Model Checking Information Flow in Reactive Systems. | Rayna Dimitrova, Bernd Finkbeiner, Mt Kovcs, Markus N. Rabe, Helmut Seidl |
| 2011 | POPL | Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. | Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Peter Lammich, Markus Mller-Olm |
| 2011 | SAS | Side-Effect Analysis of Assembly Code. | Andrea Flexeder, Michael Petter, Helmut Seidl |
| 2011 | VMCAI | Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation. | Thomas Martin Gawlitza, Peter Lammich, Markus Mller-Olm, Helmut Seidl, Alexander Wenner |
| 2010 | APLAS | Interprocedural Control Flow Reconstruction. | Andrea Flexeder, Bogdan Mihaila, Michael Petter, Helmut Seidl |
| 2010 | CADE | Abstract Interpretation over Zones without Widening. | Thomas Martin Gawlitza, Helmut Seidl |
| 2010 | DLT | Minimization of Deterministic Bottom-Up Tree Transducers. | Sylvia Friese, Helmut Seidl, Sebastian Maneth |
| 2010 | ICALP | What Is a Pure Functional? | Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl |
| 2010 | LPAR | Bottom-Up Tree Automata with Term Constraints. | Andreas Reu, Helmut Seidl |
| 2010 | SAS | Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely. | Thomas Martin Gawlitza, Helmut Seidl |
| 2010 | SAS | Verifying a Local Generic Solver in Coq. | Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl |
| 2010 | VMCAI | Shape Analysis of Low-Level C with Overlapping Structures. | Jrg Kreiker, Helmut Seidl, Vesal Vojdani |
| 2009 | CAV | Games through Nested Fixpoints. | Thomas Gawlitza, Helmut Seidl |
| 2009 | FM | A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis. | Helmut Seidl, Vesal Vojdani, Varmo Vene |
| 2009 | SAS | Region Analysis for Race Detection. | Helmut Seidl, Vesal Vojdani |
| 2008 | ESOP | Upper Adjoints for Fast Inter-procedural Variable Equalities. | Markus Mller-Olm, Helmut Seidl |
| 2008 | FM | Precise Interval Analysis vs. Parity Games. | Thomas Gawlitza, Helmut Seidl |
| 2008 | GI | Lightweight Verification 2008. | Martin Leucker, Helmut Seidl |
| 2008 | ICALP | Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations. | Javier Esparza, Thomas Gawlitza, Stefan Kiefer, Helmut Seidl |
| 2008 | SAS | Analysing All Polynomial Equations in . | Helmut Seidl, Andrea Flexeder, Michael Petter |
| 2007 | ATVA | Computing Game Values for Crash Games. | Thomas Gawlitza, Helmut Seidl |
| 2007 | CSL | Precise Relational Invariants Through Strategy Iteration. | Thomas Gawlitza, Helmut Seidl |
| 2007 | ESOP | Precise Fixpoint Computation Through Strategy Iteration. | Thomas Gawlitza, Helmut Seidl |
| 2007 | ESOP | Interprocedurally Analysing Linear Inequality Relations. | Helmut Seidl, Andrea Flexeder, Michael Petter |
| 2007 | ICDT | Exact XML Type Checking in Polynomial Time. | Sebastian Maneth, Thomas Perst, Helmut Seidl |
| 2006 | STACS | Interprocedurally Analyzing Polynomial Identities. | Markus Mller-Olm, Michael Petter, Helmut Seidl |
| 2005 | CADE | On the Complexity of Equational Horn Clauses. | Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick |
| 2005 | ESOP | Analysis of Modular Arithmetic. | Markus Mller-Olm, Helmut Seidl |
| 2005 | ESOP | Interprocedural Herbrand Equalities. | Markus Mller-Olm, Helmut Seidl, Bernhard Steffen |
| 2005 | PODS | XML type checking with macro tree transducers. | Sebastian Maneth, Alexandru Berlea, Thomas Perst, Helmut Seidl |
| 2005 | SAS | A Generic Framework for Interprocedural Analysis of Numerical Properties. | Markus Mller-Olm, Helmut Seidl |
| 2005 | VMCAI | Checking Herbrand Equalities and Beyond. | Markus Mller-Olm, Oliver Rthing, Helmut Seidl |
| 2004 | ICALP | A Note on Karr's Algorithm. | Markus Mller-Olm, Helmut Seidl |
| 2004 | ICALP | Counting in Trees for Free. | Helmut Seidl, Thomas Schwentick, Anca Muscholl, Peter Habermehl |
| 2004 | LPAR | A Generic Framework for Interprocedural Analyses of Numerical Properties. | Markus Mller-Olm, Helmut Seidl |
| 2004 | LPAR | Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying. | Helmut Seidl, Kumar Neeraj Verma |
| 2004 | POPL | Precise interprocedural analysis through linear algebra. | Markus Mller-Olm, Helmut Seidl |
| 2004 | TACAS | The Succinct Solver Suite. | Flemming Nielson, Hanne Riis Nielson, Hongyan Sun, Mikael Buchholtz, Ren Rydhof Hansen, Henrik Pilegaard, Helmut Seidl |
| 2003 | PODS | Numerical document queries. | Helmut Seidl, Thomas Schwentick, Anca Muscholl |
| 2002 | ESOP | Automatic Complexity Analysis. | Flemming Nielson, Hanne Riis Nielson, Helmut Seidl |
| 2002 | ICALP | Infinite-State High-Level MSCs: Model-Checking and Realizability. | Blaise Genest, Anca Muscholl, Helmut Seidl, Marc Zeitoun |
| 2002 | SAS | Polynomial Constants Are Decidable. | Markus Mller-Olm, Helmut Seidl |
| 2002 | SAS | Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi. | Flemming Nielson, Hanne Riis Nielson, Helmut Seidl |
| 2001 | ESOP | Control-Flow Analysis in Cubic Time. | Flemming Nielson, Helmut Seidl |
| 2001 | FOSSACS | Synchronized Tree Languages Revisited and New Applications. | Valrie Gouranton, Pierre Rty, Helmut Seidl |
| 2001 | STOC | On optimal slicing of parallel programs. | Markus Mller-Olm, Helmut Seidl |
| 2000 | ESOP | Constraint-Based Inter-Procedural Analysis of Parallel Programs. | Helmut Seidl, Bernhard Steffen |
| 1999 | CSL | On Guarding Nested Fixpoints. | Helmut Seidl, Andreas Neumann |
| 1998 | ESOP | Propagating Differences: An Efficient New Fixpoint Algorithm for Distributive Constraint Systems. | Christian Fecht, Helmut Seidl |
| 1997 | POPL | Constraints to Stop Higher-Order Deforestation. | Helmut Seidl, Morten Heine Srensen |
| 1996 | ESOP | Integer Constraints to Stop Deforestation. | Helmut Seidl |
| 1996 | LICS | A Modal Mu-Calculus for Durational Transition Systems. | Helmut Seidl |
| 1996 | SAS | An Even Faster Solver for General Systems of Equations. | Christian Fecht, Helmut Seidl |
| 1994 | ICALP | Least Solutions of Equations over N. | Helmut Seidl |
| 1989 | FCT | On the Finite Degree of Ambiguity of Finite Tree Automata. | Helmut Seidl |
| 1989 | STACS | Deciding Equivalence of Finite Tree Automata. | Helmut Seidl |
| 1986 | MFCS | On the Degree of Ambiguity of Finite Automata. | Andreas Weber, Helmut Seidl |
| 1985 | FCT | A quadratic regularity test for non-deleting macro S grammars. | Helmut Seidl |