Searcharxiv⌕ Search

arXiv subjects

Helmut Seidl

Publications and source records attributed to Helmut Seidl.

At least 19 recordsLinked to original sources
arXiv2026

Fidelity-Aware Scheduling of Quantum Circuits on Multi-QPU Systems

High Performance Computing-Quantum Computing (HPCQC) platforms expose multiple Quantum Processing Units (QPUs) that may differ in size, topology, native gates, and noise characteristics. For current noisy devices, errors compound along the compiled circuits quickly, and minimizing them, that is, maximizing the circuits' execution fidelity, is essential for reliable results. Fidelity depends on the compilation to a specific target device: the same high-level circuit may produce different executables and, therefore, different expected fidelities across QPUs. We present a low-overhead fidelity-aware scheduling framework for multi-QPU systems based on a Graph Neural Network (GNN) that estimates, before compilation, the expected fidelity of each circuit on each available QPU. Then, a tunable scheduler uses these estimates to control the trade-off between execution fidelity and parallelism. Results show that this framework allows for approximating an exhaustive fidelity-based assignment, saving computational resources compared to a brute-force approach that compiles each circuit on every device.

quant-ph↗
arXiv2026

GPU-Accelerated Host-Aware Dead-Measurement Detection in Hybrid Quantum--Classical Programs: Full Version

Hybrid programs combine a quantum circuit with a classical host program that consumes measurement outcomes. In such programs, an outcome may be syntactically read by the host but semantically non-contributory: changing the outcome cannot change the returned value. Such outcomes obscure gates that are dead only relative to the host semantics, and are therefore invisible to circuit-local optimizers. We present a semantics-aware host-side static analysis that identifies non-contributory measurement outcomes by abstract interpretation, and prove its soundness. We implement the analysis and evaluate it on $24$ application-faithful hybrid workloads across quantum chemistry, optimization, quantum machine learning, and quantum finance. Compared with a syntactic liveness baseline, our analysis identifies more than $4\times$ as many non-contributory measurements, and it standalone enables the removal of $37.98\%$ of total gates on average. Even after the state-of-the-art optimizers like Qiskit, t|ket$\rangle$, and PyZX have already optimized the circuits, our analysis still enables removal of more than $30\%$ of the post-optimized gates, showing that the host-semantic opportunities exposed by our analysis are not subsumed by circuit-local optimization. To scale our analysis, we further lower host programs to an SSA-style levelized intermediate representation that exposes level-wise parallelism for GPU execution, and implement a CUDA backend. We prove that this lowering preserves the analysis result, and the evaluation shows speedups of up to $6.53\times$ over a sequential baseline as structural parallelism increases.

quant-ph↗
arXiv2026

Max-Policy Iteration, Revisited

Max-policy iteration is an approach to computing precise numeric program invariants by successive attempts at resolving maximum operators and reduction to mathematical optimization. Mathematical optimization, though, may be expensive. Here, we show, for max-policy iteration on systems of equations over integers as well as over floating point numbers, that mathematical optimization can be replaced by plain value iteration -- which is still guaranteed to terminate. As an application, a precise bound analysis for integer or floating point variables is obtained, avoiding widening operators altogether. We also consider max-policy iteration over the rational numbers, where the right-hand sides are maxima of minima of affine combinations of unknowns. We propose min-policy iteration as an alternative to linear programming for solving the optimization problems posed by max-policy iteration. We prove that max-min policy iteration is guaranteed to return the least solution for bounded systems. We also show how to extend this algorithm to unbounded systems, and how to construct certificates of soundness as well as of optimality of the computed results.

cs.PL↗
arXiv2026

Compile-Time Simplification of Classically Controlled Operations in Dynamic Circuits

Dynamic circuits use real-time outcomes of mid-circuit measurements, processed by a classical controller, to adapt subsequent operations during circuit execution. This additional flexibility over static circuits comes at a price. Mid-circuit measurements are typically slower and noisier than unitary gates. Furthermore, classical feedforward requires exchanging information between the quantum processor (QPU) and the classical controller, introducing latency that erodes the practical performance of dynamic circuits. We propose a compile-time optimization framework that reduces the use of classical controls in dynamic circuits while preserving their semantics. At its core, the framework uses a static analysis that symbolically executes the circuit by propagating classical information alongside the quantum state. By combining this classical-quantum information with the Probabilistic Circuit Model extended with probabilistic controls that emulate classical feedforward, we obtain an intermediate probabilistic representation of the dynamic circuit. In this representation, mid-circuit measurements and classically controlled operations can be removed or rewritten as purely unitary operations and probabilistic components. Compared to existing compile-time optimizations that target only mid-circuit measurements, our method applies to a broader class of dynamic circuits expressible in modern quantum programming languages. We evaluated our framework on randomly generated dynamic circuits, achieving about 50% classical feedforward reduction and even higher reductions in favorable settings.

quant-ph↗
arXiv2026

Practical Insights into Fair Comparison and Evaluation Frame for Neutral-Atom Compilers

Neutral-atom quantum computing is among the most promising platforms for scalable quantum computation, and compilation toolchains are crucial for leveraging capabilities such as qubit shuttling and parallel gate execution. An important challenge, however, is that existing neutral-atom compilers are often evaluated using metrics computed over different parts of the toolchain and under non-equivalent assumptions. Consequently, fair quantification and comparison of compiler performance remain difficult. Reported metrics may depend on inconsistent transpilation optimization levels, different movement-duration models, different sets of considered fidelity sources, and even minor implementation bugs or undocumented representation choices. To address this problem, we present a unified and reproducible evaluation framework for neutral-atom compilers. Our framework introduces RSQASM (Routed and Scheduled QASM), a QASM-inspired post-compilation representation that captures mapped, routed, and scheduled circuits, including explicit parallel gate execution and shuttling operations. As part of the framework, we provide adapter scripts that translate existing compiler outputs and intermediate artifacts into RSQASM. As a case study, we compare three well-known neutral-atom compilation toolchains: HybridMapper, DasAtom, and Enola, motivated by the large performance differences reported in prior work. Using our framework and representation, we perform a new evaluation and show that several previously claimed performance gaps become substantially smaller and, in some cases, are not reproduced once evaluation inconsistencies are removed.

cs.ET↗
arXiv2026

Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities (Extended Version)

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.

cs.PL↗
arXiv2025

Dead Gate Elimination

Hybrid quantum algorithms combine the strengths of quantum and classical computing. Many quantum algorithms, such as the variational quantum eigensolver (VQE), leverage this synergy. However, quantum circuits are executed in full, even when only subsets of measurement outcomes contribute to subsequent classical computations. In this manuscript, we propose a novel circuit optimization technique that identifies and removes dead gates. We prove that the removal of dead gates has no influence on the probability distribution of the measurement outcomes that contribute to the subsequent calculation result. We implemented and evaluated our optimization on a VQE instance, a quantum phase estimation (QPE) instance, and hybrid programs embedded with random circuits of varying circuit width, confirming its capability to remove a non-trivial number of dead gates in real-world algorithms. The effect of our optimization scales up as more measurement outcomes are identified as non-contributory, resulting in a proportionally greater reduction of dead gates.

quant-ph↗
arXiv2025

Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses

Static analysis of real-world programs combines flow- and context-sensitive analyses of local program states with computation of flow- and context-insensitive invariants at globals, that, e.g., abstract data shared by multiple threads. The values of locals and globals may mutually depend on each other, with the analysis of local program states both making contributions to globals and querying their values. Usually, all contributions to globals are accumulated during fixpoint iteration, with widening applied to enforce termination. Such flow-insensitive information often becomes unnecessarily imprecise and can include superfluous contributions -- trash -- which, in turn, may be toxic to the precision of the overall analysis. To recover precision of globals, we propose techniques complementing each other: Narrowing on globals differentiates contributions by origin; reluctant widening limits the amount of widening applied at globals; and finally, abstract garbage collection undoes contributions to globals and propagates their withdrawal. The experimental evaluation shows that these techniques increase the precision of mixed flow-sensitive analyses at a reasonable cost.

cs.PL↗
arXiv2025

When is a Bottom-Up Deterministic Tree Translation Top-Down Deterministic?

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 whether the translation of a transducer with look-ahead can be realized by a transducer from the same class without look-ahead. The transducers constructed in this way, may still make use of inspection, i.e., have an additional tree automaton restricting the domain. We provide a second procedure which decides whether inspection can be removed. The procedure relies on a precise abstract interpretation of inspection requirements and a dedicated earliest normal form for linear as well as uniform-copying transducers which can be constructed in polynomial time. As a consequence, equivalence of these transducers can be decided in polynomial time. Applying these results to deterministic bottom-up tree transducers, we obtain that it is decidable whether or not their translations can be realized by deterministic linear or uniform-copying top-down transducers without look-ahead (but with inspection) -- or without both look-ahead and inspection. Look-ahead removal has been known to be a notoriously difficult problem. To the best of our knowledge, this paper is the first to present look-ahead removal for natural and known subclasses of top-down tree transducers.

cs.FL↗
arXiv2024

Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)

Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps underlying the verdict in an exchangeable format, enabling independent validation of the reasoning by other tools. For the correctness of concurrent programs, no agreed-upon witness format exists -- in no small part due to the divide between the semantics considered by analyzers, ranging from interleaving to thread-modular approaches, making it challenging to exchange information. We propose a format that leverages the well-known notion of ghosts to embed the claims a tool makes about a program into a modified program with ghosts, such that the validity of a witness can be decided by analyzing this program. Thus, the validity of witnesses with respect to the interleaving and the thread-modular semantics coincides. Further, thread-modular invariants computed by an abstract interpreter can naturally be expressed in the new format using ghost statements. We evaluate the approach by generating such ghost witnesses for a subset of concurrent programs from the SV-COMP benchmark suite, and pass them to a model checker. It can confirm 75% of these witnesses -- indicating that ghost witnesses can bridge the semantic divide between interleaving and thread-modular approaches.

cs.PL↗
arXiv2024

Non-Numerical Weakly Relational Domains

The weakly relational domain of Octagons offers a decent compromise between precision and efficiency for numerical properties. Here, we are concerned with the construction of non-numerical relational domains. We provide a general construction of weakly relational domains, which we exemplify with an extension of constant propagation by disjunctions. Since for the resulting domain of 2-disjunctive formulas, satisfiability is NP-complete, we provide a general construction for a further, more abstract weakly relational domain where the abstract operations of restriction and least upper bound can be efficiently implemented. In the second step, we consider a relational domain that tracks conjunctions of inequalities between variables, and between variables and constants for arbitrary partial orders of values. Examples are sub(multi)sets, as well as prefix, substring or scattered substring orderings on strings. When the partial order is a lattice, we provide precise polynomial algorithms for satisfiability, restriction, and the best abstraction of disjunction. Complementary to the constructions for lattices, we find that, in general, satisfiability of conjunctions is NP-complete. We therefore again provide polynomial abstract versions of restriction, conjunction, and join. By using our generic constructions, these domains are extended to weakly relational domains that additionally track disjunctions. For all our domains, we indicate how abstract transformers for assignments and guards can be constructed.

cs.LO↗
arXiv2023

Correctness Witness Validation by Abstract Interpretation

Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own.

cs.PL↗
arXiv2023

Checking in Polynomial Time whether or not a Regular Tree Language is Deterministic Top-Down

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 language. Recently it was claimed that such a decision can be carried out in polynomial time (Leupold and Maneth, FCT'2021); but their procedure and corresponding property is wrong. Here we correct this mistake and present a correct property which allows to determine in polynomial time whether or not a given tree language can be recognized by a deterministic top-down tree automaton. Furthermore, our new property is stated for arbitrary deterministic bottom-up tree automata, and not for minimal such automata (as before).

cs.FL↗
arXiv2023

Clustered Relational Thread-Modular Abstract Interpretation with Local Traces

We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables - given that they are protected by common mutexes. We provide a framework to systematically increase the precision of clustered relational analyses by splitting control locations based on abstractions of local traces. As one instance, we obtain an analysis of dynamic thread creation and joining. Interestingly, tracking less relational information for globals may result in higher precision. We consider the class of 2-decomposable domains that encompasses many weakly relational domains (e.g., Octagons). For these domains, we prove that maximal precision is attained already for clusters of globals of sizes at most 2.

cs.PL↗
arXiv2022

Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap

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, abstract interpretation in general can be quite costly. To achieve quick response times, we incrementalize the analysis infrastructure, including postprocessing, without necessitating any modifications to the analysis specifications themselves. We rely on the local generic fixpoint engine TD, which dynamically tracks dependencies, while exploring the unknowns contributing to answering an initial query. Lazy invalidation is employed for analysis results affected by program change. Dedicated improvements support the incremental analysis of concurrency deficiencies such as data-races. The framework has been implemented for multithreaded C within the static analyzer Goblint, using MagpieBridge to relay findings to IDEs. We evaluate our implementation w.r.t. the yard sticks of response time and consistency: formerly proven invariants should be retained - when they are not affected by the change. The results indicate that with our approach, a reanalysis after small changes only takes a fraction of from-scratch analysis time, while most of the precision is retained. We also provide examples of program development highlighting the usability of the overall approach.

cs.PL↗
arXiv2021

Improving Thread-Modular Abstract Interpretation

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 and side-effecting constraint systems. We show that a generalization of the analysis provided by the static analyzer Goblint as well as a natural improvement of Antoine Min\'e's approach can be obtained as instances of this general scheme. We show that these two analyses are incomparable w.r.t. precision and provide a refinement which improves on both precision-wise. We also report on a preliminary experimental comparison of the given analyses on a meaningful suite of benchmarks.

cs.PL↗
arXiv2021

Definability Results for Top-Down Tree Transducers

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 (2)~by a tree homomorphism. We present algorithms that construct equivalent such transducers if they exist.

cs.FL↗