Publication detail

AutoQ: An Automata-based Quantum Circuit Verifier

LENGÁL, O. CHEN, Y. TSAI, W. CHUNG, K. LIN, J.

Original Title

AutoQ: An Automata-based Quantum Circuit Verifier

Type

conference paper

Language

English

Original 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.

Keywords

quantum circuits, verification, tree automata, symbolic execution

Authors

LENGÁL, O.; CHEN, Y.; TSAI, W.; CHUNG, K.; LIN, J.

Released

19. 7. 2023

Publisher

Springer Verlag

Location

Cham

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Number

13966

State

Federal Republic of Germany

Pages from

139

Pages to

153

Pages count

15

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"
}