@inproceedings{Tao2022,
  title         = {Giallar: Push-Button Verification for the Qiskit Quantum Compiler},
  author        = {Tao, Runzhou and Shi, Yunong and Yao, Jianan and Li, Xupeng and Javadi-Abhari, Ali and Cross, Andrew W. and Chong, Frederic T. and Gu, Ronghui},
  year          = {2022},
  month         = jun,
  booktitle     = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
  publisher     = acm,
  address       = {New York, NY, USA},
  series        = {{{PLDI}} '22},
  pages         = {641--656},
  numpages      = {16},
  doi           = {10.1145/3519939.3523431},
  archiveprefix = {arXiv},
  eprint        = {2205.00661},
  abstract      = {This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewriting rules for reducing symbolic quantum circuits. With Giallar, we implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. Our evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance.},
  keywords      = {quantum computing, compiler verification, automated verification},
  webnote       = {Previously known as [CertiQ (arXiv:1908.08963)](https://arxiv.org/abs/1908.08963).},
  bibsource     = qplbib
}

{"_id":"r6wY73nHPYtvThoyv","bibbaseid":"tao-shi-yao-li-javadiabhari-cross-chong-gu-giallarpushbuttonverificationfortheqiskitquantumcompiler-2022","author_short":["Tao, R.","Shi, Y.","Yao, J.","Li, X.","Javadi-Abhari, A.","Cross, A. W.","Chong, F. T.","Gu, R."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Giallar: Push-Button Verification for the Qiskit Quantum Compiler","author":[{"propositions":[],"lastnames":["Tao"],"firstnames":["Runzhou"],"suffixes":[]},{"propositions":[],"lastnames":["Shi"],"firstnames":["Yunong"],"suffixes":[]},{"propositions":[],"lastnames":["Yao"],"firstnames":["Jianan"],"suffixes":[]},{"propositions":[],"lastnames":["Li"],"firstnames":["Xupeng"],"suffixes":[]},{"propositions":[],"lastnames":["Javadi-Abhari"],"firstnames":["Ali"],"suffixes":[]},{"propositions":[],"lastnames":["Cross"],"firstnames":["Andrew","W."],"suffixes":[]},{"propositions":[],"lastnames":["Chong"],"firstnames":["Frederic","T."],"suffixes":[]},{"propositions":[],"lastnames":["Gu"],"firstnames":["Ronghui"],"suffixes":[]}],"year":"2022","month":"June","booktitle":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","publisher":"Association for Computing Machinery","address":"New York, NY, USA","series":"PLDI '22","pages":"641–656","numpages":"16","doi":"10.1145/3519939.3523431","archiveprefix":"arXiv","eprint":"2205.00661","abstract":"This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewriting rules for reducing symbolic quantum circuits. With Giallar, we implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. Our evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance.","keywords":"quantum computing, compiler verification, automated verification","webnote":"Previously known as [CertiQ (arXiv:1908.08963)](https://arxiv.org/abs/1908.08963).","bibsource":"Quantum Programming Languages & Verification Bibliography, https://git.io/qpl-bib","bibtex":"@inproceedings{Tao2022,\n title = {Giallar: Push-Button Verification for the Qiskit Quantum Compiler},\n author = {Tao, Runzhou and Shi, Yunong and Yao, Jianan and Li, Xupeng and Javadi-Abhari, Ali and Cross, Andrew W. and Chong, Frederic T. and Gu, Ronghui},\n year = {2022},\n month = jun,\n booktitle = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},\n publisher = acm,\n address = {New York, NY, USA},\n series = {{{PLDI}} '22},\n pages = {641--656},\n numpages = {16},\n doi = {10.1145/3519939.3523431},\n archiveprefix = {arXiv},\n eprint = {2205.00661},\n abstract = {This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewriting rules for reducing symbolic quantum circuits. With Giallar, we implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. Our evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance.},\n keywords = {quantum computing, compiler verification, automated verification},\n webnote = {Previously known as [CertiQ (arXiv:1908.08963)](https://arxiv.org/abs/1908.08963).},\n bibsource = qplbib\n}\n\n","author_short":["Tao, R.","Shi, Y.","Yao, J.","Li, X.","Javadi-Abhari, A.","Cross, A. W.","Chong, F. T.","Gu, R."],"key":"Tao2022","id":"Tao2022","bibbaseid":"tao-shi-yao-li-javadiabhari-cross-chong-gu-giallarpushbuttonverificationfortheqiskitquantumcompiler-2022","role":"author","urls":{},"keyword":["quantum computing","compiler verification","automated verification"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/QuantumPL/bib/main/bbt.bib","dataSources":["JG9W34HAXfSxsC6ML"],"keywords":["quantum computing","compiler verification","automated verification"],"search_terms":["giallar","push","button","verification","qiskit","quantum","compiler","tao","shi","yao","li","javadi-abhari","cross","chong","gu"],"title":"Giallar: Push-Button Verification for the Qiskit Quantum Compiler","year":2022}