{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:43:35Z","timestamp":1742982215863,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031517761"},{"type":"electronic","value":"9783031517778"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-51777-8_5","type":"book-chapter","created":{"date-parts":[[2024,1,12]],"date-time":"2024-01-12T09:03:07Z","timestamp":1705050187000},"page":"68-84","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Automated Quantum Program Verification in\u00a0Dynamic Quantum Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9890-1015","authenticated-orcid":false,"given":"Tsubasa","family":"Takagi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1601-4584","authenticated-orcid":false,"given":"Canh Minh","family":"Do","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,1,13]]},"reference":[{"key":"5_CR1","unstructured":"Akatov, D.: The logic of quantum program verification. Master\u2019s thesis, Oxford University (2005)"},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1017\/S0960129506005299","volume":"16","author":"A Baltag","year":"2006","unstructured":"Baltag, A., Smets, S.: LQP: the dynamic logic of quantum information. Math. Struct. Comput. Sci. 16(3), 491\u2013525 (2006)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"10","key":"5_CR3","doi-asserted-by":"publisher","first-page":"3628","DOI":"10.1007\/s10773-013-1987-3","volume":"53","author":"A Baltag","year":"2014","unstructured":"Baltag, A., Bergfeld, J., Kishida, K., Sack, J., Smets, S., Zhong, S.: PLQP & company: decidable logics for quantum algorithms. Int. J. Theor. Phys. 53(10), 3628\u20133647 (2014)","journal-title":"Int. J. Theor. Phys."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Baltag, A., Smets, S.: Reasoning about quantum information: an overview of quantum dynamic logic. Appli. Sci. 12(9) (2022)","DOI":"10.3390\/app12094458"},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"1895","DOI":"10.1103\/PhysRevLett.70.1895","volume":"70","author":"CH Bennett","year":"1993","unstructured":"Bennett, C.H., Brassard, G., Cr\u00e9peau, C., Jozsa, R., Peres, A., Wootters, W.K.: Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Phys. Rev. Lett. 70, 1895\u20131899 (1993)","journal-title":"Phys. Rev. Lett."},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"2881","DOI":"10.1103\/PhysRevLett.69.2881","volume":"69","author":"CH Bennett","year":"1992","unstructured":"Bennett, C.H., Wiesner, S.J.: Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states. Phys. Rev. Lett. 69, 2881\u20132884 (1992)","journal-title":"Phys. Rev. Lett."},{"issue":"6","key":"5_CR7","doi-asserted-by":"publisher","first-page":"1421","DOI":"10.1007\/s00500-015-1802-6","volume":"21","author":"JM Bergfeld","year":"2017","unstructured":"Bergfeld, J.M., Sack, J.: Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs. Soft. Comput. 21(6), 1421\u20131441 (2017)","journal-title":"Soft. Comput."},{"issue":"7671","key":"5_CR8","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1038\/nature23474","volume":"549","author":"J Biamonte","year":"2017","unstructured":"Biamonte, J., Wittek, P., Pancotti, N., Rebentrost, P., Wiebe, N., Lloyd, S.: Quantum machine learning. Nature 549(7671), 195\u2013202 (2017)","journal-title":"Nature"},{"issue":"4","key":"5_CR9","doi-asserted-by":"publisher","first-page":"823","DOI":"10.2307\/1968621","volume":"57","author":"G Birkhoff","year":"1936","unstructured":"Birkhoff, G., von Neumann, J.: The logic of quantum mechanics. Ann. Math. 57(4), 823\u2013843 (1936)","journal-title":"Ann. Math."},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Do, C.M., Ogata, K.: Symbolic model checking quantum circuits in maude. In: The 35th International Conference on Software Engineering and Knowledge Engineering, SEKE 2023 (2023)","DOI":"10.18293\/SEKE2023-014"},{"issue":"5516","key":"5_CR12","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1126\/science.1057726","volume":"292","author":"E Farhi","year":"2001","unstructured":"Farhi, E., Goldstone, J., Gutmann, S., Lapan, J., Lundgren, A., Preda, D.: A quantum adiabatic evolution algorithm applied to random instances of an np-complete problem. Science 292(5516), 472\u2013475 (2001)","journal-title":"Science"},{"key":"5_CR13","unstructured":"Gay, S., Nagarajan, R., Papanikolaou, N.: Probabilistic model-checking of quantum protocols. arXiv preprint quant-ph\/0504007 (2005)"},{"issue":"6760","key":"5_CR14","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1038\/46503","volume":"402","author":"D Gottesman","year":"1999","unstructured":"Gottesman, D., Chuang, I.L.: Demonstrating the viability of universal quantum computation using teleportation and single-qubit operations. Nature 402(6760), 390\u2013393 (1999)","journal-title":"Nature"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Hardegree, G.M.: The conditional in quantum logic. Synthese, 63\u201380 (1974)","DOI":"10.1007\/BF00484952"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"5_CR17","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502","volume":"103","author":"AW Harrow","year":"2009","unstructured":"Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum algorithm for linear systems of equations. Phys. Rev. Lett. 103, 150502 (2009)","journal-title":"Phys. Rev. Lett."},{"issue":"3","key":"5_CR18","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1305\/ndjfl\/1093891789","volume":"16","author":"L Herman","year":"1975","unstructured":"Herman, L., Marsden, E.L., Piziak, R.: Implication connectives in orthomodular lattices. Notre Dame J. Formal Logic 16(3), 305\u2013328 (1975)","journal-title":"Notre Dame J. Formal Logic"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"1829","DOI":"10.1103\/PhysRevA.59.1829","volume":"59","author":"M Hillery","year":"1999","unstructured":"Hillery, M., Bu\u017eek, V., Berthiaume, A.: Quantum secret sharing. Phys. Rev. A 59, 1829\u20131834 (1999)","journal-title":"Phys. Rev. A"},{"issue":"7\u20138","key":"5_CR20","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebraic Methods Program 81(7\u20138), 721\u2013781 (2012)","journal-title":"J. Log. Algebraic Methods Program"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511976667"},{"issue":"1","key":"5_CR22","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1145\/3093333.3009894","volume":"52","author":"J Paykin","year":"2017","unstructured":"Paykin, J., Rand, R., Zdancewic, S.: Qwire: a core language for quantum circuits. SIGPLAN Not. 52(1), 846\u2013858 (2017)","journal-title":"SIGPLAN Not."},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"R\u00e9dei, M.: Quantum logic in algebraic approach. FTPH, vol. 91. Springer (1998). https:\/\/doi.org\/10.1007\/978-94-015-9026-6","DOI":"10.1007\/978-94-015-9026-6"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Shor, P.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings 35th Annual Symposium on Foundations of Computer Science, pp. 124\u2013134 (1994)","DOI":"10.1109\/SFCS.1994.365700"},{"issue":"6","key":"5_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2049706.2049708","volume":"33","author":"M Ying","year":"2012","unstructured":"Ying, M.: Floyd-hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 33(6), 1\u201349 (2012)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"4","key":"5_CR26","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s00236-010-0117-4","volume":"47","author":"M Ying","year":"2010","unstructured":"Ying, M., Feng, Y.: Quantum loop programs. Acta Informatica 47(4), 221\u2013250 (2010)","journal-title":"Acta Informatica"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Ying, M., Feng, Y.: Model checking quantum systems \u2013 a survey (2018)","DOI":"10.1093\/nsr\/nwy106"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"\u017bukowski, M., Zeilinger, A., Horne, M.A., Ekert, A.K.: \u201cEvent-ready-detectors\u201d Bell experiment via entanglement swapping. Phys. Rev. Lett. 71, 4287\u20134290 (1993)","DOI":"10.1103\/PhysRevLett.71.4287"}],"container-title":["Lecture Notes in Computer Science","Dynamic Logic. New Trends and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-51777-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,7]],"date-time":"2024-11-07T23:08:45Z","timestamp":1731020925000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-51777-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031517761","9783031517778"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-51777-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"13 January 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"DaL\u00ed","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Dynamic Logic","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tbilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"DaL\u00ed2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/dali2023.compute.dtu.dk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"80% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}