QPMC: A model checker for quantum programs and protocols

Yuan Feng; Ernst Moritz Hahn; Andrea Turrini; Lijun Zhang

doi:10.1007/978-3-319-19249-9_17

QPMC: A model checker for quantum programs and protocols

Yuan Feng, Ernst Moritz Hahn, Andrea Turrini^*, Lijun Zhang

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

26 Citations (Scopus)

Abstract

We present QPMC (Quantum Program/Protocol Model Checker), an extension of the probabilistic model checker ISCASMC to automatically verify quantum programs and quantum protocols. QPMC distinguishes itself from the previous quantum model checkers proposed in the literature in that it works for general quantum programs and protocols, not only those using Clifford operations. A command-line version of QPMC is available at http://iscasmc.ios.ac.cn/tool/qmc/.

Original language	English
Title of host publication	FM 2015: Formal Methods
Subtitle of host publication	20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings
Editors	Nikolaj Bjorner, Frank de Boer
Place of Publication	Cham
Publisher	Springer
Pages	265-272
Number of pages	8
ISBN (Electronic)	978-3-319-19249-9
ISBN (Print)	978-3-319-19248-2
DOIs	https://doi.org/10.1007/978-3-319-19249-9_17
Publication status	Published - 2015
Externally published	Yes
Event	20th International Symposium on Formal Methods, FM 2015 - Oslo, Norway Duration: 24 Jun 2015 → 26 Jun 2015 Conference number: 20

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9109
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	20th International Symposium on Formal Methods, FM 2015
Abbreviated title	FM
Country/Territory	Norway
City	Oslo
Period	24/06/15 → 26/06/15

Keywords

Model checker
Quantum cryptography
Physical review letter
Discrete time Markov chain
Kraus operator

Access to Document

10.1007/978-3-319-19249-9_17

Cite this

@inproceedings{6c4a99c65722470583f8b0b07fe94dbc,

title = "QPMC: A model checker for quantum programs and protocols",

abstract = "We present QPMC (Quantum Program/Protocol Model Checker), an extension of the probabilistic model checker ISCASMC to automatically verify quantum programs and quantum protocols. QPMC distinguishes itself from the previous quantum model checkers proposed in the literature in that it works for general quantum programs and protocols, not only those using Clifford operations. A command-line version of QPMC is available at http://iscasmc.ios.ac.cn/tool/qmc/.",

keywords = "Model checker, Quantum cryptography, Physical review letter, Discrete time Markov chain, Kraus operator",

author = "Yuan Feng and Hahn, {Ernst Moritz} and Andrea Turrini and Lijun Zhang",

year = "2015",

doi = "10.1007/978-3-319-19249-9_17",

language = "English",

isbn = "978-3-319-19248-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "265--272",

editor = "Nikolaj Bjorner and {de Boer}, Frank",

booktitle = "FM 2015: Formal Methods",

address = "Germany",

note = "20th International Symposium on Formal Methods, FM 2015, FM ; Conference date: 24-06-2015 Through 26-06-2015",

}

Feng, Y, Hahn, EM, Turrini, A & Zhang, L 2015, QPMC: A model checker for quantum programs and protocols. in N Bjorner & F de Boer (eds), FM 2015: Formal Methods: 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9109, Springer, Cham, pp. 265-272, 20th International Symposium on Formal Methods, FM 2015, Oslo, Norway, 24/06/15. https://doi.org/10.1007/978-3-319-19249-9_17

QPMC: A model checker for quantum programs and protocols. / Feng, Yuan; Hahn, Ernst Moritz; Turrini, Andrea et al.
FM 2015: Formal Methods: 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. ed. / Nikolaj Bjorner; Frank de Boer. Cham: Springer, 2015. p. 265-272 (Lecture Notes in Computer Science; Vol. 9109).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - QPMC

T2 - 20th International Symposium on Formal Methods, FM 2015

AU - Feng, Yuan

AU - Hahn, Ernst Moritz

AU - Turrini, Andrea

AU - Zhang, Lijun

N1 - Conference code: 20

PY - 2015

Y1 - 2015

N2 - We present QPMC (Quantum Program/Protocol Model Checker), an extension of the probabilistic model checker ISCASMC to automatically verify quantum programs and quantum protocols. QPMC distinguishes itself from the previous quantum model checkers proposed in the literature in that it works for general quantum programs and protocols, not only those using Clifford operations. A command-line version of QPMC is available at http://iscasmc.ios.ac.cn/tool/qmc/.

AB - We present QPMC (Quantum Program/Protocol Model Checker), an extension of the probabilistic model checker ISCASMC to automatically verify quantum programs and quantum protocols. QPMC distinguishes itself from the previous quantum model checkers proposed in the literature in that it works for general quantum programs and protocols, not only those using Clifford operations. A command-line version of QPMC is available at http://iscasmc.ios.ac.cn/tool/qmc/.

KW - Model checker

KW - Quantum cryptography

KW - Physical review letter

KW - Discrete time Markov chain

KW - Kraus operator

UR - http://www.scopus.com/inward/record.url?scp=84937402028&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-19249-9_17

DO - 10.1007/978-3-319-19249-9_17

M3 - Conference contribution

SN - 978-3-319-19248-2

T3 - Lecture Notes in Computer Science

SP - 265

EP - 272

BT - FM 2015: Formal Methods

A2 - Bjorner, Nikolaj

A2 - de Boer, Frank

PB - Springer

CY - Cham

Y2 - 24 June 2015 through 26 June 2015

ER -

QPMC: A model checker for quantum programs and protocols

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this