Publication Details

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

HSIEH Min-hsiu, HUANG Wei-jia, CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao and TSAI Wei-lun. AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs. In: Proceedings of TACAS'25. Springer Verlag, 2025. ISSN 0302-9743.
Czech title
AutoQ 2.0: Od verifikace kvantových obvodů k verifikaci kvantových programů
Type
conference paper
Language
english
Authors
Hsieh Min-hsiu (FOXCONN)
Huang Wei-jia (FOXCONN)
Chen Yu-Fang (ASIN)
Chung Kai-Min (ASIN)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Lin Jyun-ao (ASIN)
Tsai Wei-lun (ASIN)
Keywords

quantum programs
tree automata
measurement
verification

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.

Published
2025 (in print)
Journal
Lecture Notes in Computer Science, ISSN 0302-9743
Proceedings
Proceedings of TACAS'25
Conference
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems --- TACAS'25, Hamilton, CA
Publisher
Springer Verlag
BibTeX 
@INPROCEEDINGS{FITPUB13385,
   author = "Min-hsiu Hsieh and Wei-jia Huang and Yu-Fang Chen and Kai-Min Chung and Ond\v{r}ej Leng\'{a}l and Jyun-ao Lin and Wei-lun Tsai",
   title = "AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs",
   booktitle = "Proceedings of TACAS'25",
   journal = "Lecture Notes in Computer Science",
   year = 2025,
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13385"
}
Back to top