Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Lecture notes in computer science

Equivalence Checking in Multi-level Quantum Systems

Philipp Niemann, Robert Wille, Rolf Drechsler

Published Jan 1, 2014• 43 citations
Publisher
DOI
10.1007/978-3-319-08494-7_16

Related papers

Equivalence Checking of Quantum Protocols

Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan

Lecture notes in computer science•Jan 1, 2013•35 citations

Equivalence checking of quantum finite-state machines

Qisheng Wang, Junyi Liu, Mingsheng Ying

arXiv:1901.02173•Journal of Computer and System Sciences•Sep 17, 2020•5 citations

Verification of Concurrent Quantum Protocols by Equivalence Checking

Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan

Lecture notes in computer science•Jan 1, 2014•33 citations

Equivalence Checking of Quantum Circuits with the ZX-Calculus

Lukas Burgholzer, Robert Wille

Springer eBooks•Jan 1, 2026•0 citations

Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation ofVariational Quantum Algorithms

Lukas Burgholzer, Robert Wille

Springer eBooks•Jan 1, 2026•0 citations

Quantum Circuit Equivalence Checking: A Tractable Bridge From Unitary to Hybrid Circuits

Jérome Ricciardi, Sébastien Bardin, Christophe Chareton +1 more

Equivalence checking of hybrid quantum circuits is of primary importance, given that quantum circuit transformations are omnipresent along the quantum compiler chain. While some approaches exist for automating this task, most focus on the simple case of unitary circuits. At the same time, real quantum computing requires hybrid circuits equipped with measurement operators. Moreover, the few approaches targeting the hybrid case are limited to a restricted class of problems. We propose tackling the Quantum Hybrid Circuit Equivalence Checking problem through lifting unitary circuit verification using a transformation known as deferred measurement. We show that this approach alone significantly outperforms prior work, and that, with the addition of specific unitary-level techniques we call separation and projection, it can handle much larger classes of hybrid circuit equivalence problems. We have implemented and evaluated our method over standard circuit transformations such as teleportation, one-way measurement, or the IBM Qiskit compiler, demonstrating its promises. As a side finding, we have identified and reported several unexpected behaviours with the Qiskit compiler.

quant-pharXiv:2511.22523•Nov 28, 2025•1 citation
Equivalence checking of hybrid quantum circuits is of primary importance, given that quantum circuit transformations are omnipresent along the quantum compiler chain. While some approaches exist for automating this task, most focus on the simple case of unitary circuits. At the same time, real quantum computing requires hybrid circuits equipped with measurement operators. Moreover, the few approaches targeting the hybrid case are limited to a restricted class of problems. We propose tackling the Quantum Hybrid Circuit Equivalence Checking problem through lifting unitary circuit verification using a transformation known as deferred measurement. We show that this approach alone significantly outperforms prior work, and that, with the addition of specific unitary-level techniques we call separation and projection, it can handle much larger classes of hybrid circuit equivalence problems. We have implemented and evaluated our method over standard circuit transformations such as teleportation, one-way measurement, or the IBM Qiskit compiler, demonstrating its promises. As a side finding, we have identified and reported several unexpected behaviours with the Qiskit compiler.