Publikation: symQV : Automated Symbolic Verification of Quantum Programs
Lade...
Dateien
Datum
2023
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
oops
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen 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_12
Zusammenfassung
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 224-dimensional state space).
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Quantum computing, Formal verification, Symbolic execution, Abstraction
Konferenz
25th International Symposium on Formal Methods : FM 2023, 6. März 2023 - 10. März 2023, Lübeck
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690
BAUER-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_12BibTex
@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} }
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<sup>24</sup>-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>
Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja