Publikation:

symQV : Automated Symbolic Verification of Quantum Programs

Lade...
Vorschaubild

Dateien

Bauer-Marquart_2-43spemd6cbbe5.pdf
Bauer-Marquart_2-43spemd6cbbe5.pdfGröße: 266.15 KBDownloads: 32

Datum

2023

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

ArXiv-ID

Internationale Patentnummer

Link zur Lizenz
oops

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz

Gesperrt bis

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

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690BAUER-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_12
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}
}
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>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
Begutachtet
Diese Publikation teilen