We present a tool QSeqSim, a Qiskit-integrated symbolic backend that fills the current gap of having no Qiskit-native support for simulating while-loop quantum programs and their induced sequential quantum circuits. QSeqSim takes Qiskit QuantumCircuit objects, translates them into OpenQASM 3 code, and organises the resulting program into a combination of combinational, dynamic, and sequential circuits, thereby assigning while-loops a precise sequential circuit semantics with explicit internal and external qubits. Building on this semantics, QSeqSim adopts a Binary Decision Diagram (BDD)-based symbolic representation and integrates weighted model counting to compute measurement probabilities efficiently by exploiting sharing in structured and sparse BDDs. On top of this Boolean backbone, it introduces dedicated symbolic operators for state composition and state retention, thereby enabling efficient symbolic execution of sequential quantum circuits. Our experiments demonstrate that QSeqSim scales to substantial while-induced sequential circuits; in particular, in the quantum random walk benchmark we successfully simulate circuits with over 1000 qubits for more than 10 loop iterations.
QSeqSim is available at https://github.com/Veri-Q/QSeqSim.
This is the full arXiv version of the paper accepted at FM 2026. The paper has 26 pages and 4 figures. Proceedings version: FM 2026, LNCS 16556, Springer, 2026
We present a tool QSeqSim, a Qiskit-integrated symbolic backend that fills the current gap of having no Qiskit-native support for simulating while-loop quantum programs and their induced sequential quantum circuits. QSeqSim takes Qiskit QuantumCircuit objects, translates them into OpenQASM 3 code, and organises the resulting program into a combination of combinational, dynamic, and sequential circuits, thereby assigning while-loops a precise sequential circuit semantics with explicit internal and external qubits. Building on this semantics, QSeqSim adopts a Binary Decision Diagram (BDD)-based symbolic representation and integrates weighted model counting to compute measurement probabilities efficiently by exploiting sharing in structured and sparse BDDs. On top of this Boolean backbone, it introduces dedicated symbolic operators for state composition and state retention, thereby enabling efficient symbolic execution of sequential quantum circuits. Our experiments demonstrate that QSeqSim scales to substantial while-induced sequential circuits; in particular, in the quantum random walk benchmark we successfully simulate circuits with over 1000 qubits for more than 10 loop iterations.
Quantum circuit simulation is the basic tool for reasoning over quantum programs. Despite the tremendous advance in the simulator technology in the recent years, the performance of simulators is still unsatisfactory on non-trivial circuits, which slows down the development of new quantum systems. In this work, we develop a loop summarizing simulator based on multi-terminal binary decision diagrams (MTBDDs) with efficiently customized quantum gate operations. The simulator is capable of automatic loop summarization using symbolic execution, which saves repetitive computation for circuits with iterative structures. Experimental results show the simulator outperforms state-of-the-art simulators on some standard circuits, such as Grover's algorithm, by several orders of magnitude.
In this paper, we introduce VeriQBench -- an open source benchmark for quantum circuits. It offers high-level quantum circuit abstractions of various circuit types, including 1) combinational, 2) dynamic, 3) sequential, and 4) variational quantum circuits, which cover almost all existing types of quantum circuits in the literature. Meanwhile, VeriQBench is a versatile benchmark which can be used in verifying quantum software for different applications, as is evidenced by the existing works including quantum circuit verification (e.g., equivalence checking [Hon+21a; WLY21] and model checking [Yin21]), simulation (e.g., fault simulation), testing (e.g., test pattern generation [CY22]) and debugging (e.g., runtime assertions [Li+20b]). All the circuits are described in OpenQASM and are validated on Qiskit and QCOR simulators. With the hope that it can be used by other researchers, VeriQBench is released at: https://github.com/Veri-Q/Benchmark.
Abstract The simulation of quantum circuits on classical computers is an important problem in quantum computing. Such simulation requires representations of distributions over very large sets of basis vectors, and recent work has used symbolic data-structures such as Binary Decision Diagrams (BDDs) for this purpose. In this tool paper, we present Quasimodo, an extensible, open-source Python library for symbolic simulation of quantum circuits. Quasimodo is specifically designed for easy extensibility to other backends. Quasimodo allows simulations of quantum circuits, checking properties of the outputs of quantum circuits, and debugging quantum circuits. It also allows the user to choose from among several symbolic data-structures—both unweighted and weighted BDDs, and a recent structure called Context-Free-Language Ordered Binary Decision Diagrams (CFLOBDDs)—and can be easily extended to support other symbolic data-structures.
Reproducibility and comparability remain fundamental challenges in the empirical evaluation of Quantum Software Engineering (QSE) tools. These challenges arise from the intrinsic probabilistic behavior of quantum programs and the variability introduced by quantum hardware and simulator backends. While existing quantum benchmarks typically offer only static circuit definitions, they often leave researchers responsible for data generation and execution, hindering the creation of standardized and reproducible experiments. In this paper, we introduce QSimBench, a novel, open-source benchmark suite and accompanying Python library designed to address these limitations. QSimBench provides over 20 million precomputed shot-level execution traces:20,000measurements each, across14quantum algorithms, multiple circuit sizes (4−15qubits), and six Qiskit-based backends including both ideal and noise-injected simulations. Each configuration includes not only detailed measurement histories but also the original circuit in OpenQASM, the backend's noise model, and configuration metadata, ensuring full transparency and enabling in-depth analysis. QSimBench empowers researchers to conduct scalable, reproducible, and statistically rigorous evaluations of QSE tools, such as those for monitoring, orchestration, and statistical post-processing, without the need for expensive or difficult-to-reproduce quantum executions. The benchmark is distributed with a lightweight Python API that facilitates fast data retrieval, flexible sampling strategies, and seamless integration into experimental pipelines. QSimBench is publicly available, aiming to foster collaborative and reproducible research within the quantum software community.
The classical simulation of universal quantum circuits is crucial both fundamentally and practically for quantum computation. We propose SyQMA, a simulator with several convenient features, particularly suited for quantum error correction (QEC). SyQMA simulates universal quantum circuits with incoherent Pauli noise and computes exact expectation values and measurement probabilities as symbolic functions of circuit parameters: rotation angles, measurement outcomes, and noise rates. This simulator can sample measurement outcomes, enabling the simulation of dynamic quantum programs where circuit composition depends on prior measurement outputs. For QEC, it performs circuit-level maximum-likelihood decoding, provides exact symbolic expressions for logical error rates, and verifies the fault distance of fault-tolerant (FT) stabiliser and magic state preparation protocols. These features are enabled by an intuitive extension of stabiliser simulators, where each non-Clifford Pauli rotation and incoherent Pauli channel is compactly represented via auxiliary qubits and a modified trace. Representing the state requires only polynomial memory and time, while computing expectation values and measurement probabilities takes exponential time in the number of non-Clifford rotations and deterministic measurements, but only polynomial memory. The FT preparation of stabiliser and magic states, including the first stage of magic state cultivation, is analysed without approximations. We also exactly convert the disjoint error probabilities of a general multi-qubit Pauli channel to independent ones, a key step for creating and sampling from detector error models. The code is publicly available and open-source.
This work presents QiliSim, the native C++ simulation backend of QiliSDK, an open-source Python framework for digital and analog quantum computing. QiliSim supports quantum circuits, Hamiltonian time evolution, and analog-digital quantum reservoirs through a common interface, allowing users to test quantum algorithms before executing them on quantum hardware. The simulator provides statevector and density-matrix methods for digital workloads, alongside fixed-step and adaptive Runge–Kutta integrators, Krylov-subspace methods, and direct matrix exponentiation for analog evolution. Monte Carlo trajectories, mid-circuit measurements, and Kraus and Lindbladian noise models support the simulation of noisy quantum systems. Numerical methods and execution settings are selected through structured configuration objects, allowing the same quantum program to run with different simulation strategies without modifying its definition. The poster includes a circuit simulation example and performance comparisons for digital circuit sampling and quantum annealing. The reported benchmarks show competitive CPU performance against Qiskit Aer and Cirq for small to medium circuits, and faster execution than QuTiP and CUDA-Q dynamics for the tested annealing task at a target fidelity of 99%.