Abstract We present a verifier of quantum programs called AutoQ 2.0. Quantum programs extend quantum circuits (the domain of AutoQ 1.0) by classical control flow constructs, which enable users to describe advanced quantum algorithms in a formal and precise manner. The extension is highly non-trivial, as we needed to tackle both theoretical challenges (such as the treatment of measurement, the normalization problem, and lifting techniques for verification of classical programs with loops to the quantum world), and engineering issues (such as extending the input format with a support for specifying loop invariants). We have successfully used AutoQ 2.0 to verify two types of advanced quantum programs that cannot be expressed using only quantum circuits: the repeat-until-success (RUS) algorithm and the weak-measurement-based version of Grover’s search algorithm. AutoQ 2.0 can efficiently verify all our benchmarks: all RUS algorithms were verified instantly and, for the weak-measurement-based version of Grover’s search, we were able to handle the case of 100 qubits in $$\sim $$ ∼ 20 minutes.
Abstract We present a verifier of quantum programs called AutoQ 2.0. Quantum programs extend quantum circuits (the domain of AutoQ 1.0) by classical control flow constructs, which enable users to describe advanced quantum algorithms in a formal and precise manner. The extension is highly non-trivial, as we needed to tackle both theoretical challenges (such as the treatment of measurement, the normalization problem, and lifting techniques for verification of classical programs with loops to the quantum world), and engineering issues (such as extending the input format with a support for specifying loop invariants). We have successfully used AutoQ 2.0 to verify two types of advanced quantum programs that cannot be expressed using only quantum circuits: the repeat-until-success (RUS) algorithm and the weak-measurement-based version of Grover’s search algorithm. AutoQ 2.0 can efficiently verify all our benchmarks: all RUS algorithms were verified instantly and, for the weak-measurement-based version of Grover’s search, we were able to handle the case of 100 qubits in ∼ ∼ 20 minutes.
We present a verifier of quantum programs called AutoQ 2.0. Quantum programs extend quantum circuits (the domain of AutoQ 1.0) by classical control flow constructs, which enable users to describe advanced quantum algorithms in a formal and precise manner. The extension is highly non-trivial, as we needed to tackle both theoretical challenges (such as the treatment of measurement, the normalization problem, and lifting techniques for verification of classical programs with loops to the quantum world), and engineering issues (such as extending the input format with a~support for specifying loop invariants). We have successfully used AutoQ 2.0 to verify two types of advanced quantum programs that cannot be expressed using only quantum circuits: the \emph{repeat-until-success} (RUS) algorithm and the weak-measurement-based version of Grover's search algorithm. AutoQ 2.0 can efficiently verify all our benchmarks: all RUS algorithms were verified instantly and, for the weak-measurement-based version of Grover's search, we were able to handle the case of 100 qubits in $\sim$20 minutes.
Abstract We present a specification language and a fully automated tool named AutoQ for verifying quantum circuits symbolically. The tool implements the automata-based algorithm from [14] and extends it with the capabilities for symbolic reasoning. The extension allows to specify relational properties, i.e., relationships between states before and after executing a circuit. We present a number of use cases where we used AutoQ to fully automatically verify crucial properties of several quantum circuits, which have, to the best of our knowledge, so far been proved only with human help.
An efficient and intuitive format of quantum programs is an indispensable component to handle large-scale quantum computers. Representing and manipulating a sequence of quantum instructions as a network of quantum gates, i.e., quantum circuits, is one of the most successful approaches. Quantum circuits are intuitive since there are similar representations in classical engineering, such as electric or digital circuits. However, due to their differences from these classical circuits, naively automated manipulation and optimization for quantum circuit networks easily tend to an ill-defined format. To avoid this problem, a flexible and verifiable network format of quantum circuits is strongly demanded. In this extended poster abstract, we propose a representation with these properties, named quantum circuit fragments. In our representation, the connectivity of several types of wires in quantum circuits, qubit, control, and measurement-feedback wiring, are kept as three sets. We also provide a linear time algorithm to validate that our format can be converted to quantum circuits. Using our preliminary software to treat quantum circuit fragments, Q-Divide, we demonstrated that code complexity can be halved in practical cases. Thus, our work improves the efficiency of quantum computer development and motivates further exploration for efficient representation and manipulation of large-scale quantum programs.
ABSTRACT- This paper presents an integrated framework for the automated verification and visualization of quantum circuits, addressing the critical need for reliable quantum software development tools. We implement and analyze eight fundamental quantum circuits Bell states, GHZ states, Quantum Fourier Transform (QFT), Grover's search algorithm, the Variational Quantum Eigensolver (VQE) for H₂ molecules, Quantum Teleportation, Superdense Coding, and the Bernstein-Vazirani algorithm through a comprehensive verification pipeline. The system generates publication-ready circuit diagrams and performs formal verification via automated theorem proving, achieving an overall verification success rate of 93.7% across all circuits. Notably, basic circuits such as Bell and GHZ states achieve perfect verification (100% success), whereas the Quantum Teleportation circuit presents the greatest challenge, attaining only 88.9% success. Results demonstrate a strong linear correlation (R² = 0.89) between circuit complexity (gate count) and verification time, with the framework processing 348 verification conditions per second. This work establishes quantitative benchmarks for quantum software verification, highlights specific gaps in protocol-level verification, and provides an integrated toolset that bridges the gap between circuit visualization and formal correctness assurance, thereby advancing the state of quantum software engineering.
Quantum technologies are progressing at an extraordinary pace and are poised to transform numerous sectors both nationally and globally. Among them, quantum computing stands out for its potential to revolutionize areas such as cryptography, optimization, and the simulation of quantum systems, offering dramatic speed-ups for specific classes of problems. As quantum devices evolve and become increasingly pervasive, guaranteeing their correctness is of paramount importance. This necessitates the development of rigorous methods and tools to analyze and verify their behavior. However, the construction of such verification frameworks presents fundamental challenges. Quantum phenomena such as superposition and entanglement give rise to computational behaviors that differ profoundly from those of classical systems, leading to inherently probabilistic models and exponentially large state spaces, even for relatively small programs. Addressing these challenges requires building on the extensive expertise of the formal methods community in classical program verification, while incorporating recent advances and collaborative efforts in quantum systems. An interesting challenge for the verification community is to design and implement novel verification frameworks that transfer the key strengths of classical verification, such as expressive specification, precise error detection, automation, and scalability, to the quantum domain. We expect that the results of this research will play a crucial role in enabling the dependable deployment of quantum technologies across a wide range of future applications.
Abstract While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor’s integer factoring, quantum phase estimation (QPE) and Grover’s search.