{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T16:21:06Z","timestamp":1781108466473,"version":"3.54.1"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319192482","type":"print"},{"value":"9783319192499","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_17","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"265-272","source":"Crossref","is-referenced-by-count":24,"title":["QPMC: A Model Checker for Quantum Programs and Protocols"],"prefix":"10.1007","author":[{"given":"Yuan","family":"Feng","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ernst Moritz","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-36742-7_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Ardeshir-Larijani","year":"2013","unstructured":"Ardeshir-Larijani, E., Gay, S., Nagarajan, R.: Equivalence checking of quantum protocols. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 478\u2013492. Springer, Heidelberg (2013)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-54862-8_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Ardeshir-Larijani","year":"2014","unstructured":"Ardeshir-Larijani, E., Gay, S., Nagarajan, R.: Verification of concurrent quantum protocols by equivalence checking. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol.\u00a08413, pp. 500\u2013514. Springer, Heidelberg (2014)"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"3121","DOI":"10.1103\/PhysRevLett.68.3121","volume":"68","author":"C.H. Bennett","year":"1992","unstructured":"Bennett, C.H.: Quantum cryptography using any two nonorthogonal states. Physical Review Letters\u00a068, 3121 (1992)","journal-title":"Physical Review Letters"},{"key":"17_CR4","unstructured":"Bennett, C.H., Brassard, G.: Quantum cryptography: Public-key distribution and coin tossing. In: Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing, pp. 175\u2013179 (1984)"},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"1895","DOI":"10.1103\/PhysRevLett.70.1895","volume":"70","author":"C.H. Bennett","year":"1993","unstructured":"Bennett, C.H., Brassard, G., Crepeau, C., Jozsa, R., Peres, A., Wootters, W.: Teleporting an unknown quantum state via dual classical and EPR channels. Physical Review Letters\u00a070, 1895\u20131899 (1993)","journal-title":"Physical Review Letters"},{"issue":"20","key":"17_CR6","doi-asserted-by":"publisher","first-page":"2881","DOI":"10.1103\/PhysRevLett.69.2881","volume":"69","author":"C.H. Bennett","year":"1992","unstructured":"Bennett, C.H., Wiesner, S.J.: Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states. Physical Review Letters\u00a069(20), 2881\u20132884 (1992)","journal-title":"Physical Review Letters"},{"issue":"11","key":"17_CR7","doi-asserted-by":"publisher","first-page":"1608","DOI":"10.1016\/j.ic.2007.08.001","volume":"205","author":"Y. Feng","year":"2007","unstructured":"Feng, Y., Duan, R., Ji, Z., Ying, M.: Probabilistic bisimulations for quantum processes. Information and Computation\u00a0205(11), 1608\u20131639 (2007)","journal-title":"Information and Computation"},{"issue":"4","key":"17_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2400676.2400680","volume":"34","author":"Y. Feng","year":"2012","unstructured":"Feng, Y., Duan, R., Ying, M.: Bisimulation for Quantum Processes. ACM Transactions on Programming Languages and Systems\u00a034(4), 1\u201343 (2012)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"7","key":"17_CR9","doi-asserted-by":"publisher","first-page":"1181","DOI":"10.1016\/j.jcss.2013.04.002","volume":"79","author":"Y. Feng","year":"2013","unstructured":"Feng, Y., Yu, N., Ying, M.: Model checking quantum Markov chains. Journal of Computer and System Sciences\u00a079(7), 1181\u20131198 (2013)","journal-title":"Journal of Computer and System Sciences"},{"key":"17_CR10","unstructured":"Gay, S., Nagarajan, R., Papanikolaou, N.: Probabilistic model-checking of quantum protocols. In: Proceedings of the 2nd International Workshop on Developments in Computational Models (2006)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-540-70545-1_51","volume-title":"Computer Aided Verification","author":"S.J. Gay","year":"2008","unstructured":"Gay, S.J., Nagarajan, R., Papanikolaou, N.: QMC: A model checker for quantum systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 543\u2013547. Springer, Heidelberg (2008)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"E.M. Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: A web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol.\u00a08442, pp. 312\u2013317. Springer, Heidelberg (2014)"},{"key":"17_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12732-1","volume-title":"States, Effects and Operations: Fundamental Notions of Quantum Theory","author":"K. Kraus","year":"1983","unstructured":"Kraus, K.: States, Effects and Operations: Fundamental Notions of Quantum Theory. Springer, Berlin (1983)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"issue":"3","key":"17_CR15","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/382780.382781","volume":"48","author":"D. Mayers","year":"2001","unstructured":"Mayers, D.: Unconditional security in quantum cryptography. Journal of the ACM\u00a048(3), 351\u2013406 (2001)","journal-title":"Journal of the ACM"},{"key":"17_CR16","unstructured":"Nielsen, M., Chuang, I.: Quantum computation and quantum information. Cambridge university press (2000)"},{"issue":"4","key":"17_CR17","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1017\/S0960129504004256","volume":"14","author":"P. Selinger","year":"2004","unstructured":"Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science\u00a014(4), 527\u2013586 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"17_CR18","volume-title":"Mathematical Foundations of Quantum Mechanics","author":"J. von Neumann","year":"1955","unstructured":"von Neumann, J.: Mathematical Foundations of Quantum Mechanics. Princeton University Press, Princeton (1955)"},{"issue":"3","key":"17_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1507244.1507249","volume":"10","author":"M. Ying","year":"2009","unstructured":"Ying, M., Feng, Y., Duan, R., Ji, Z.: An algebra of quantum processes. ACM Transactions on Computational Logic (TOCL)\u00a010(3), 1\u201336 (2009)","journal-title":"ACM Transactions on Computational Logic (TOCL)"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T12:23:00Z","timestamp":1675858980000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}