symQV: Automated Symbolic Verification of Quantum Programs. Bauer-Marquart, F., Leue, S., & Schilling, C. In Chechik, M., Katoen, J., & Leucker, M., editors, Formal Methods, of Lecture Notes in Computer Science, pages 181–198, Cham, 2023. Springer International Publishing. doi abstract bibtex We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a symbolic quantum program model. This allows to encode the verification problem in an SMT formula, which can then be checked with a $$\mathbf \delta $$-complete decision procedure. We also propose an abstraction technique to speed up the verification process. Experimental results show that the abstraction improves symQV ’s scalability by an order of magnitude to quantum programs with 24 qubits (a $$ 2\textasciicircum\24\$$-dimensional state space).
@inproceedings{bauer-marquart_symqv_2023,
address = {Cham},
series = {Lecture {Notes} in {Computer} {Science}},
title = {{symQV}: {Automated} {Symbolic} {Verification} of {Quantum} {Programs}},
isbn = {978-3-031-27481-7},
shorttitle = {{symQV}},
doi = {10.1007/978-3-031-27481-7_12},
abstract = {We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a symbolic quantum program model. This allows to encode the verification problem in an SMT formula, which can then be checked with a \$\${\textbackslash}mathbf {\textbackslash}delta \$\$-complete decision procedure. We also propose an abstraction technique to speed up the verification process. Experimental results show that the abstraction improves symQV ’s scalability by an order of magnitude to quantum programs with 24 qubits (a \$\$ 2{\textasciicircum}\{24\}\$\$-dimensional state space).},
language = {en},
booktitle = {Formal {Methods}},
publisher = {Springer International Publishing},
author = {Bauer-Marquart, Fabian and Leue, Stefan and Schilling, Christian},
editor = {Chechik, Marsha and Katoen, Joost-Pieter and Leucker, Martin},
year = {2023},
keywords = {Abstraction, Formal verification, Quantum computing, Symbolic execution},
pages = {181--198},
}
Downloads: 0
{"_id":"46xLTktnfQScwFxWG","bibbaseid":"bauermarquart-leue-schilling-symqvautomatedsymbolicverificationofquantumprograms-2023","author_short":["Bauer-Marquart, F.","Leue, S.","Schilling, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Cham","series":"Lecture Notes in Computer Science","title":"symQV: Automated Symbolic Verification of Quantum Programs","isbn":"978-3-031-27481-7","shorttitle":"symQV","doi":"10.1007/978-3-031-27481-7_12","abstract":"We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a symbolic quantum program model. This allows to encode the verification problem in an SMT formula, which can then be checked with a $$\\mathbf \\delta $$-complete decision procedure. We also propose an abstraction technique to speed up the verification process. Experimental results show that the abstraction improves symQV ’s scalability by an order of magnitude to quantum programs with 24 qubits (a $$ 2\\textasciicircum\\24\\$$-dimensional state space).","language":"en","booktitle":"Formal Methods","publisher":"Springer International Publishing","author":[{"propositions":[],"lastnames":["Bauer-Marquart"],"firstnames":["Fabian"],"suffixes":[]},{"propositions":[],"lastnames":["Leue"],"firstnames":["Stefan"],"suffixes":[]},{"propositions":[],"lastnames":["Schilling"],"firstnames":["Christian"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Chechik"],"firstnames":["Marsha"],"suffixes":[]},{"propositions":[],"lastnames":["Katoen"],"firstnames":["Joost-Pieter"],"suffixes":[]},{"propositions":[],"lastnames":["Leucker"],"firstnames":["Martin"],"suffixes":[]}],"year":"2023","keywords":"Abstraction, Formal verification, Quantum computing, Symbolic execution","pages":"181–198","bibtex":"@inproceedings{bauer-marquart_symqv_2023,\n\taddress = {Cham},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {{symQV}: {Automated} {Symbolic} {Verification} of {Quantum} {Programs}},\n\tisbn = {978-3-031-27481-7},\n\tshorttitle = {{symQV}},\n\tdoi = {10.1007/978-3-031-27481-7_12},\n\tabstract = {We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a symbolic quantum program model. This allows to encode the verification problem in an SMT formula, which can then be checked with a \\$\\${\\textbackslash}mathbf {\\textbackslash}delta \\$\\$-complete decision procedure. We also propose an abstraction technique to speed up the verification process. Experimental results show that the abstraction improves symQV ’s scalability by an order of magnitude to quantum programs with 24 qubits (a \\$\\$ 2{\\textasciicircum}\\{24\\}\\$\\$-dimensional state space).},\n\tlanguage = {en},\n\tbooktitle = {Formal {Methods}},\n\tpublisher = {Springer International Publishing},\n\tauthor = {Bauer-Marquart, Fabian and Leue, Stefan and Schilling, Christian},\n\teditor = {Chechik, Marsha and Katoen, Joost-Pieter and Leucker, Martin},\n\tyear = {2023},\n\tkeywords = {Abstraction, Formal verification, Quantum computing, Symbolic execution},\n\tpages = {181--198},\n}\n\n\n\n\n\n\n\n","author_short":["Bauer-Marquart, F.","Leue, S.","Schilling, C."],"editor_short":["Chechik, M.","Katoen, J.","Leucker, M."],"key":"bauer-marquart_symqv_2023","id":"bauer-marquart_symqv_2023","bibbaseid":"bauermarquart-leue-schilling-symqvautomatedsymbolicverificationofquantumprograms-2023","role":"author","urls":{},"keyword":["Abstraction","Formal verification","Quantum computing","Symbolic execution"],"metadata":{"authorlinks":{}},"downloads":0,"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/alukina","dataSources":["Cfgnp5s4HQSBd8tAf"],"keywords":["abstraction","formal verification","quantum computing","symbolic execution"],"search_terms":["symqv","automated","symbolic","verification","quantum","programs","bauer-marquart","leue","schilling"],"title":"symQV: Automated Symbolic Verification of Quantum Programs","year":2023}