English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We introduce a new paradigm for analysing and finding bugs in quantumcircuits. In our approach, the problem is given by a triple $\{P\}\,C\,\{Q\}$and the question is whether, given a set $P$ of quantum states on the input ofa circuit $C$, the set of quantum states on the output is equal to (or includedin) a set $Q$. While this is not suitable to specify, e.g., functionalcorrectness of a quantum circuit, it is sufficient to detect many bugs inquantum circuits. We propose a technique based on tree automata to compactlyrepresent sets of quantum states and develop transformers to implement thesemantics of quantum gates over this representation. Our technique computeswith an algebraic representation of quantum states, avoiding the inaccuracy ofworking with floating-point numbers. We implemented the proposed approach in aprototype tool and evaluated its performance against various benchmarks fromthe literature. The evaluation shows that our approach is quite scalable, e.g.,we managed to verify a large circuit with 40 qubits and 141,527 gates, or catchbugs injected into a circuit with 320 qubits and 1,758 gates, where all toolswe compared with failed. In addition, our work establishes a connection betweenquantum program verification and automata, opening new possibilities to exploitthe richness of automata theory and automata-based verification in the world ofquantum computing.

An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits (Technical Report)