Detail výsledku

AutoQ: An Automata-based Quantum Circuit Verifier

LENGÁL, O.; CHEN, Y.; TSAI, W.; CHUNG, K.; LIN, J. AutoQ: An Automata-based Quantum Circuit Verifier. In Proceedings of 35th International Conference on Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer Verlag, 2023. no. 13966, p. 139-153. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Chen Yu-Fang
TSAI, W.
CHUNG, K.
LIN, J.
Abstrakt

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.

Klíčová slova

quantum circuits, verification, tree automata, symbolic execution

Rok
2023
Strany
139–153
Časopis
Lecture Notes in Computer Science, č. 13966, ISSN 0302-9743
Sborník
Proceedings of 35th International Conference on Computer Aided Verification
Konference
35th International Conference on Computer Aided Verification
Vydavatel
Springer Verlag
Místo
Cham
DOI
10.1007/978-3-031-37709-9_7
EID Scopus
2-s2.0-85169429472
BibTeX 
@inproceedings{BUT185179,
  author="LENGÁL, O. and CHEN, Y. and TSAI, W. and CHUNG, K. and LIN, J.",
  title="AutoQ: An Automata-based Quantum Circuit Verifier",
  booktitle="Proceedings of 35th International Conference on Computer Aided Verification",
  year="2023",
  journal="Lecture Notes in Computer Science",
  number="13966",
  pages="139--153",
  publisher="Springer Verlag",
  address="Cham",
  doi="10.1007/978-3-031-37709-9\{_}7",
  issn="0302-9743"
}
Projekty
Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, zahájení: 2020-01-01, ukončení: 2024-12-31, ukončen
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, zahájení: 2023-03-01, ukončení: 2026-02-28, řešení
Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury, GAČR, Standardní projekty, GA23-07565S, zahájení: 2023-01-01, ukončení: 2025-12-31, řešení
Výzkumné skupiny
Automata@FIT (VZ Automata@FIT)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru