Abstract We present a theory of Cartesian arrays, which are multi-dimensional arrays with support for the projection of arrays to sub-arrays, as well as for updating sub-arrays. The resulting logic is an extension of Combinatorial Array Logic (CAL) and is motivated by the analysis of quantum circuits: using projection, we can succinctly encode the semantics of quantum gates as quantifier-free formulas and verify the end-to-end correctness of quantum circuits. Since the logic is expressive enough to represent quantum circuits succinctly, it necessarily has a high complexity; as we show, it suffices to encode thek-color problem of a graph under a succinct circuit representation, an NEXPTIME-complete problem. We present an NEXPTIME decision procedure for the logic and report on preliminary experiments with the analysis of quantum circuits using this decision procedure.
Abstract We present a theory of Cartesian arrays, which are multi-dimensional arrays with support for the projection of arrays to sub-arrays, as well as for updating sub-arrays. The resulting logic is an extension of Combinatorial Array Logic (CAL) and is motivated by the analysis of quantum circuits: using projection, we can succinctly encode the semantics of quantum gates as quantifier-free formulas and verify the end-to-end correctness of quantum circuits. Since the logic is expressive enough to represent quantum circuits succinctly, it necessarily has a high complexity; as we show, it suffices to encode thek-color problem of a graph under a succinct circuit representation, an NEXPTIME-complete problem. We present an NEXPTIME decision procedure for the logic and report on preliminary experiments with the analysis of quantum circuits using this decision procedure.
Quantum circuit verification is a critical yet notoriously challenging task in quantum computing. Full simulation of quantum circuits scales exponentially with the number of qubits and circuit depth, rendering it impractical for even moderately sized circuits. This paper proposes a novel approach to automated theorem proving for quantum circuit verification leveraging abstract interpretation. Our core idea is to approximate the behavior of quantum circuits using abstract interpretations, significantly reducing the computational complexity of the verification process. We outline a framework where abstract domains are constructed to represent the key properties of quantum circuits, such as qubit state fidelities and gate operations. The framework then employs logical reasoning and inference rules based on these abstract representations to automatically determine the correctness of a circuit against a given specification. We demonstrate the feasibility of this approach and discuss its potential to dramatically improve the efficiency and scalability of quantum circuit verification. The key benefit lies in shifting the verification burden from exact simulation to a more tractable abstract analysis.
Most contemporary quantum programming languages describe computation as circuits, using a host classical counterpart to drive the execution of quantum programs. However, the circuit model adds expensive complexity to quantum algorithmic development and decreases the transparency of connections between syntax and formal semantics in quantum programs. We argue that producing a high-level quantum programming language without reference to circuits is possible and necessary. We summarize desirable features in future high-level quantum programming languages and provide evidence supporting array pro-gramming languages as a natural paradigm for quantum algorithmic expression at the circuit level and beyond. We highlight why APL is a profitable host programming language to attain this goal progressively. In particular, we demonstrate how features provided by APL, such as native support of complex numbers and matrix operations, naturally capture quan-tum operations while bringing a less cluttered syntax that encodes and encapsulates the linear character of quantum circuit execution. We discuss implementation details of quAPL, an APL library for quantum circuit specification, simulation, and execution intended to provide a gradual ramp toward developing composable procedural abstractions. Finally, we discuss the broader implications of our work and the next steps in our research program.
The main contribution of this paper is the introduction of a dynamic logic formalism for reasoning about information flow in composite quantum systems. This builds on our previous work on a complete quantum dynamic logic for single systems. Here we extend that work to a sound (but not necessarily complete) logic for composite systems, which brings together ideas from the quantum logic tradition with concepts from (dynamic) modal logic and from quantum computation. This Logic of Quantum Programs (LQP) is capable of expressing important features of quantum measurements and unitary evolutions of multi-partite states, as well as giving logical characterisations to various forms of entanglement (for example, the Bell states, the GHZ states etc.). We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness proofs for the Teleportation protocol and for a standard Quantum Secret Sharing protocol; a whole range of other quantum circuits and programs, including other well-known protocols (for example, superdense coding, entanglement swapping, logic-gate teleportation etc.), can be similarly verified using our logic.
Rydberg atom arrays natively encode the maximum-weight independent set (MWIS) problem through the blockade mechanism, so the Boolean circuit satisfiability problem (Circuit-SAT) can be brought onto the platform once it is reduced to MWIS. The conventional encoding of Circuit-SAT in the Rydberg atom array proceeds through conjunctive normal form (CNF) and incurs a substantial atom overhead. We introduce CAMERA (Circuit-SAT Atom-efficient MWIS Encoding for Rydberg Arrays), a method that provides MWIS encodings of Circuit-SAT instances on the king subgraph geometry of the array. CAMERA represents each logic gate as a compact weighted gadget and assembles the gadgets with a placement and routing compiler inspired by very large scale integration (VLSI) design. On random multi-gate benchmarks, the direct encoding route lowers the atom cost relative to the CNF route by an average factor of 22.4±1.8. To demonstrate that the encoding extends from individual weighted gadgets to multi-gate arithmetic blocks, we compile a full adder and a multiplier, verifying each against its complete truth table by exact classical ground state calculations. We further showcase solving a representative Circuit-SAT instance end-to-end, from gate level compilation through a closed-system tensor-network simulation of a hardware-compatible annealing protocol on the encoded 30-atom instance to readout of a satisfying assignment. These results establish a complete encoding and simulation workflow as a proof of principle, and a concrete route toward solving a broader family of combinatorial problems on Rydberg atom arrays.
The main contribution of this paper is the introduction of a dynamic logic formalism for reasoning about information flow in composite quantum systems. This builds on our previous work on a complete quantum dynamic logic for single systems. Here we extend that work to a sound (but not necessarily complete) logic for composite systems, which brings together ideas from the quantum logic tradition with concepts from (dynamic) modal logic and from quantum computation. This Logic of Quantum Programs (LQP) is capable of expressing important features of quantum measurements and unitary evolutions of multi-partite states, as well as giving logical characterisations to various forms of entanglement (for example, the Bell states, the GHZ states etc.). We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness proofs for the Teleportation protocol and for a standard Quantum Secret Sharing protocol; a whole range of other quantum circuits and programs, including other well-known protocols (for example, superdense coding, entanglement swapping, logic-gate teleportation etc.), can be similarly verified using our logic.
Quantum computing exploits the principles of quantum mechanics to perform computation by manipulating qubit states through sequences of quantum gates, known as quantum circuits. As quantum hardware continues to scale in both complexity and qubit count, conventional verification techniques quickly become computationally impractical, motivating the need for more advanced verification approaches. Formal methods, including theorem proving, model checking, and symbolic reasoning, offer systematic and mathematically rigorous techniques for verifying functional correctness, equivalence, and implementation, while enabling early detection of design errors. This review explores how formal methods are currently applied to the verification of quantum circuits, with a particular focus on barrier certificates, abstract interpretation, model checking, theorem proving, and emerging hybrid approaches. Examining the theoretical foundations and practical applications of these techniques, discussing their strengths, limitations, and comparative effectiveness through representative case studies, review hopes to provide a holistic understanding of the topic. Highlighting the open challenges and outlining promising directions for future research, the review aims to provide a roadmap towards more scalable and robust verification frameworks for quantum computing. For readers seeking deeper engagement, the review offers an extensive set of references to support further study and exploration.