Papers › Verification of Quantum Circuits through Discrete-Time Barrier Certificates
Verification of Quantum Circuits through Discrete-Time Barrier Certificates
Marco Lewis, Sadegh Soudjani, Paolo Zuliani
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
Current methods for verifying quantum computers are predominately based on interactive or automatic theorem provers. Considering that quantum computers are dynamical in nature, this paper employs and extends the concepts from the verification of dynamical systems to verify properties of quantum circuits. Our main contribution is to propose k-inductive barrier certificates over complex variables and show how to compute them using Hermitian Sum of Squares optimization. We apply this new technique to verify properties of different quantum circuits.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections