AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F26%3A0196845" target="_blank" >RIV/00216305:26230/26:0196845 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.1007/978-3-031-90660-2_5" target="_blank" >http://dx.doi.org/10.1007/978-3-031-90660-2_5</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-90660-2_5" target="_blank" >10.1007/978-3-031-90660-2_5</a>

Result language

angličtina

Original language name

AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2025

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Proceedings of TACAS'25

ISBN

—

ISSN

0302-9743

e-ISSN

—

Number of pages

22

Pages from-to

87-108

Publisher name

Springer Verlag

Place of publication

Heidelberg

Event location

Hamilton

Event date

May 3, 2025

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—