symQV : Automated Symbolic Verification of Quantum Programs

Kurzanzeige
dc.contributor.authorBauer-Marquart, Fabian
dc.contributor.authorLeue, Stefan
dc.contributor.authorSchilling, Christian
dc.date.accessioned2023-04-19T11:07:31Z
dc.date.available2023-04-19T11:07:31Z
dc.date.issued2023
dc.description.abstractWe 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 δ-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 224-dimensional state space).
dc.description.versionpublisheddeu
dc.identifier.doi10.1007/978-3-031-27481-7_12
dc.identifier.ppn1843168596
dc.identifier.urihttps://kops.uni-konstanz.de/handle/123456789/66673
dc.language.isoeng
dc.subjectQuantum computing
dc.subjectFormal verification
dc.subjectSymbolic execution
dc.subjectAbstraction
dc.subject.ddc004
dc.titlesymQV : Automated Symbolic Verification of Quantum Programseng
dc.typeINPROCEEDINGS
dspace.entity.typePublication
kops.citation.bibtex
@inproceedings{BauerMarquart2023symQV-66673,
  year={2023},
  doi={10.1007/978-3-031-27481-7_12},
  title={symQV : Automated Symbolic Verification of Quantum Programs},
  number={14000},
  isbn={978-3-031-27480-0},
  publisher={Springer},
  address={Cham},
  series={Lecture Notes in Computer Science},
  booktitle={Formal Methods : 25th International Symposium, FM 2023, Proceedings},
  pages={181--198},
  editor={Chechik, Marsha and Katoen, Joost-Pieter and Leucker, Martin},
  author={Bauer-Marquart, Fabian and Leue, Stefan and Schilling, Christian}
}
kops.citation.iso690BAUER-MARQUART, Fabian, Stefan LEUE, Christian SCHILLING, 2023. symQV : Automated Symbolic Verification of Quantum Programs. 25th International Symposium on Formal Methods : FM 2023. Lübeck, 6. März 2023 - 10. März 2023. In: CHECHIK, Marsha, ed., Joost-Pieter KATOEN, ed., Martin LEUCKER, ed.. Formal Methods : 25th International Symposium, FM 2023, Proceedings. Cham: Springer, 2023, pp. 181-198. Lecture Notes in Computer Science. 14000. ISBN 978-3-031-27480-0. Available under: doi: 10.1007/978-3-031-27481-7_12deu
kops.citation.iso690BAUER-MARQUART, Fabian, Stefan LEUE, Christian SCHILLING, 2023. symQV : Automated Symbolic Verification of Quantum Programs. 25th International Symposium on Formal Methods : FM 2023. Lübeck, Mar 6, 2023 - Mar 10, 2023. In: CHECHIK, Marsha, ed., Joost-Pieter KATOEN, ed., Martin LEUCKER, ed.. Formal Methods : 25th International Symposium, FM 2023, Proceedings. Cham: Springer, 2023, pp. 181-198. Lecture Notes in Computer Science. 14000. ISBN 978-3-031-27480-0. Available under: doi: 10.1007/978-3-031-27481-7_12eng
kops.citation.rdf
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/66673">
    <dc:creator>Schilling, Christian</dc:creator>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/66673"/>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/66673/1/Bauer-Marquart_2-43spemd6cbbe5.pdf"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:issued>2023</dcterms:issued>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2023-04-19T11:07:31Z</dcterms:available>
    <dc:contributor>Schilling, Christian</dc:contributor>
    <dcterms: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 δ-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&lt;sup&gt;24&lt;/sup&gt;-dimensional state space).</dcterms:abstract>
    <dc:language>eng</dc:language>
    <dc:creator>Bauer-Marquart, Fabian</dc:creator>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2023-04-19T11:07:31Z</dc:date>
    <dc:contributor>Bauer-Marquart, Fabian</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/66673/1/Bauer-Marquart_2-43spemd6cbbe5.pdf"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:title>symQV : Automated Symbolic Verification of Quantum Programs</dcterms:title>
    <dc:contributor>Leue, Stefan</dc:contributor>
  </rdf:Description>
</rdf:RDF>
kops.conferencefield25th International Symposium on Formal Methods : FM 2023, 6. März 2023 - 10. März 2023, Lübeckdeu
kops.date.conferenceEnd2023-03-10
kops.date.conferenceStart2023-03-06
kops.description.openAccessopenaccessgreen
kops.flag.knbibliographytrue
kops.identifier.nbnurn:nbn:de:bsz:352-2-43spemd6cbbe5
kops.location.conferenceLübeck
kops.sourcefieldCHECHIK, Marsha, ed., Joost-Pieter KATOEN, ed., Martin LEUCKER, ed.. <i>Formal Methods : 25th International Symposium, FM 2023, Proceedings</i>. Cham: Springer, 2023, pp. 181-198. Lecture Notes in Computer Science. 14000. ISBN 978-3-031-27480-0. Available under: doi: 10.1007/978-3-031-27481-7_12deu
kops.sourcefield.plainCHECHIK, Marsha, ed., Joost-Pieter KATOEN, ed., Martin LEUCKER, ed.. Formal Methods : 25th International Symposium, FM 2023, Proceedings. Cham: Springer, 2023, pp. 181-198. Lecture Notes in Computer Science. 14000. ISBN 978-3-031-27480-0. Available under: doi: 10.1007/978-3-031-27481-7_12deu
kops.sourcefield.plainCHECHIK, Marsha, ed., Joost-Pieter KATOEN, ed., Martin LEUCKER, ed.. Formal Methods : 25th International Symposium, FM 2023, Proceedings. Cham: Springer, 2023, pp. 181-198. Lecture Notes in Computer Science. 14000. ISBN 978-3-031-27480-0. Available under: doi: 10.1007/978-3-031-27481-7_12eng
kops.title.conference25th International Symposium on Formal Methods : FM 2023
relation.isAuthorOfPublication9a21b382-a42d-4787-b6f9-d7e5cc48aa9e
relation.isAuthorOfPublicationa0cf1380-ebf9-403b-a02e-6e97bae25ef6
relation.isAuthorOfPublicationecb6e671-5807-41bc-bb31-f07a9b7a7c63
relation.isAuthorOfPublication.latestForDiscovery9a21b382-a42d-4787-b6f9-d7e5cc48aa9e
source.bibliographicInfo.fromPage181
source.bibliographicInfo.seriesNumber14000
source.bibliographicInfo.toPage198
source.contributor.editorChechik, Marsha
source.contributor.editorKatoen, Joost-Pieter
source.contributor.editorLeucker, Martin
source.identifier.isbn978-3-031-27480-0
source.publisherSpringer
source.publisher.locationCham
source.relation.ispartofseriesLecture Notes in Computer Science
source.titleFormal Methods : 25th International Symposium, FM 2023, Proceedings

Dateien

Originalbündel

Gerade angezeigt 1 - 1 von 1
Vorschaubild nicht verfügbar
Name:
Bauer-Marquart_2-43spemd6cbbe5.pdf
Größe:
266.15 KB
Format:
Adobe Portable Document Format
Bauer-Marquart_2-43spemd6cbbe5.pdf
Bauer-Marquart_2-43spemd6cbbe5.pdfGröße: 266.15 KBDownloads: 287

Sammlungen

Informatik und Informationswissenschaft: Publikationen