Publication Details

AutoQ: An Automata-based Quantum Circuit Verifier

CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao and TSAI Wei-lun. AutoQ: An Automata-based Quantum Circuit Verifier. In: Proceedings of 35th International Conference on Computer Aided Verification. Cham: Springer Verlag, 2023, pp. 139-153. ISSN 0302-9743.
Czech title
AutoQ: verifikátor kvantových obvodů založený na automatech
Type
conference paper
Language
english
Authors
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 circuits, verification, tree automata, symbolic execution

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 [Chen et al. 2023] 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.

Published
2023
Pages
139-153
Journal
Lecture Notes in Computer Science, no. 13966, ISSN 0302-9743
Proceedings
Proceedings of 35th International Conference on Computer Aided Verification
Conference
35th International Conference on Computer Aided Verification, Paříž, FR
Publisher
Springer Verlag
Place
Cham, DE
DOI
10.1007/978-3-031-37709-9_7
EID Scopus
2-s2.0-85169429472
BibTeX 
@INPROCEEDINGS{FITPUB13022,
   author = "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: An Automata-based Quantum Circuit Verifier",
   pages = "139--153",
   booktitle = "Proceedings of 35th International Conference on Computer Aided Verification",
   journal = "Lecture Notes in Computer Science",
   number = 13966,
   year = 2023,
   location = "Cham, DE",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-031-37709-9\_7",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13022"
}
Back to top