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

Springer eBooks

Efficient Verification of Results from Quantum Circuit Compilation Flows

Lukas Burgholzer, Robert Wille

Published Jan 1, 2026• 0 citations
Publisher
DOI
10.1007/978-3-032-06770-8_15

Related papers

An Efficient Circuit Compilation Flow for Quantum Approximate Optimization Algorithm

Alam Mahabubul, Saki Abdullah Ash, Swaroop Ghosh

IEEE Conference Proceedings•Jan 1, 2020•0 citations

CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler

Yunong Shi, Runzhou Tao, Li, Xupeng +4 more

We present CertiQ, a verification framework for writing and verifying compiler passes of Qiskit, the most widely-used quantum compiler. To our knowledge, CertiQ is the first effort enabling the verification of real-world quantum compiler passes in a mostly-automated manner. Compiler passes written in the CertiQ interface with annotations can be used to generate verification conditions, as well as the executable code that can be integrated into Qiskit. CertiQ introduces the quantum circuit calculus to enable the efficient checking of equivalence of quantum circuits by encoding such a checking procedure into an SMT problem. CertiQ also provides a verified library of widely-used data structures, transformation functions for circuits, and conversion functions for different quantum data representations. This verified library not only enables modular verification but also sheds light on future quantum compiler design. We have re-implemented and verified 26 (out of 30) Qiskit compiler passes in CertiQ, during which three bugs are detected in the Qiskit implementation. Our verified compiler pass implementations passed all of Qiskit's regression tests without showing noticeable performance loss.

arXiv:1908.08963•Aug 23, 2019•10 citations

Automated Reasoning in Quantum Circuit Compilation

Dimitrios Thanos, Alejandro Villoria, Sebastiaan Brand +4 more

Lecture notes in computer science•Oct 12, 2024•4 citations

Automating the Comparison of Quantum Compilers for Quantum Circuits

Marie Salm, Johanna Barzen, Frank Leymann +2 more

Communications in computer and information science•Jan 1, 2021•30 citations

Giallar: push-button verification for the qiskit Quantum compiler

Runzhou Tao, Yunong Shi, Jianan Yao +5 more

This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewrite rules for showing the equivalence of symbolic quantum circuits. With Giallar, we implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. Our evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance.

arXiv:2205.00661•ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)•Jun 2, 2022•47 citations

Quantum Circuit Compilation: An Emerging Application for Automated Reasoning

Davide Venturelli, N. Minh, Bryan O’Gorman +6 more

•Apr 11, 2019•29 citations
We present CertiQ, a verification framework for writing and verifying compiler passes of Qiskit, the most widely-used quantum compiler. To our knowledge, CertiQ is the first effort enabling the verification of real-world quantum compiler passes in a mostly-automated manner. Compiler passes written in the CertiQ interface with annotations can be used to generate verification conditions, as well as the executable code that can be integrated into Qiskit. CertiQ introduces the quantum circuit calculus to enable the efficient checking of equivalence of quantum circuits by encoding such a checking procedure into an SMT problem. CertiQ also provides a verified library of widely-used data structures, transformation functions for circuits, and conversion functions for different quantum data representations. This verified library not only enables modular verification but also sheds light on future quantum compiler design. We have re-implemented and verified 26 (out of 30) Qiskit compiler passes in CertiQ, during which three bugs are detected in the Qiskit implementation. Our verified compiler pass implementations passed all of Qiskit's regression tests without showing noticeable performance loss.
This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewrite rules for showing the equivalence of symbolic quantum circuits. With Giallar, we implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. Our evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance.