{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T05:12:45Z","timestamp":1772601165527,"version":"3.50.1"},"reference-count":25,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T00:00:00Z","timestamp":1772323200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T00:00:00Z","timestamp":1772323200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T00:00:00Z","timestamp":1772323200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T00:00:00Z","timestamp":1772323200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T00:00:00Z","timestamp":1772323200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T00:00:00Z","timestamp":1772323200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T00:00:00Z","timestamp":1772323200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62372312"],"award-info":[{"award-number":["62372312"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62272323"],"award-info":[{"award-number":["62272323"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62272322"],"award-info":[{"award-number":["62272322"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62372311"],"award-info":[{"award-number":["62372311"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Logical and Algebraic Methods in Programming"],"published-print":{"date-parts":[[2026,3]]},"DOI":"10.1016\/j.jlamp.2025.101108","type":"journal-article","created":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T15:25:43Z","timestamp":1767281143000},"page":"101108","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Formal reasoning about Bernstein-Vazirani algorithm"],"prefix":"10.1016","volume":"149","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-1513-1823","authenticated-orcid":false,"given":"Hongxia","family":"Sun","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3562-8602","authenticated-orcid":false,"given":"Zhiping","family":"Shi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0005-0837-5215","authenticated-orcid":false,"given":"Shanyan","family":"Chen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3176-317X","authenticated-orcid":false,"given":"Guohui","family":"Wang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8991-2756","authenticated-orcid":false,"given":"Ximeng","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2373-2779","authenticated-orcid":false,"given":"Yong","family":"Guan","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"10","key":"10.1016\/j.jlamp.2025.101108_bib0001","doi-asserted-by":"crossref","first-page":"5981","DOI":"10.1002\/int.22538","article-title":"Delay optimization for ternary fixed polarity Reed\u2013Muller circuits based on multilevel adaptive quantum genetic algorithm","volume":"36","author":"Zhenxue","year":"2021","journal-title":"Int. J. Intell. Syst."},{"issue":"1","key":"10.1016\/j.jlamp.2025.101108_bib0002","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/spe.3039","article-title":"Quantum computing: a taxonomy, systematic review and future directions","volume":"52","author":"Gill","year":"2022","journal-title":"Softw. Pract. Exp."},{"key":"10.1016\/j.jlamp.2025.101108_bib0003","series-title":"Theory of Computing","first-page":"212","article-title":"A fast quantum mechanical algorithm for database search","author":"Grover","year":"1996"},{"issue":"8","key":"10.1016\/j.jlamp.2025.101108_bib0004","doi-asserted-by":"crossref","DOI":"10.1007\/s42979-024-03505-w","article-title":"An explorative cross sectional comprehensive survey on quantum computing","volume":"5","author":"Nanda","year":"2024","journal-title":"SN Comput. Sci."},{"issue":"1818","key":"10.1016\/j.jlamp.2025.101108_bib0005","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1098\/rspa.1985.0070","article-title":"Quantum theory, the Church\u2013Turing principle and the universal quantum computer","volume":"400","author":"Deutsch","year":"1985","journal-title":"Proc. R. Soc. Lond. A"},{"issue":"1907","key":"10.1016\/j.jlamp.2025.101108_bib0006","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1098\/rspa.1992.0167","article-title":"Rapid solution of problems by quantum computation","volume":"439","author":"Deutsch","year":"1992","journal-title":"Proc. R. Soc. Lond. A"},{"key":"10.1016\/j.jlamp.2025.101108_bib0007","series-title":"Theory of Computing","first-page":"11","article-title":"Quantum complexity theory","author":"Bernstein","year":"1993"},{"key":"10.1016\/j.jlamp.2025.101108_bib0008","series-title":"Foundations of Computer Science","first-page":"124","article-title":"Algorithms for quantum computation: discrete logarithms and factoring","author":"Shor","year":"1994"},{"issue":"6","key":"10.1016\/j.jlamp.2025.101108_bib0009","doi-asserted-by":"crossref","DOI":"10.1103\/PhysRevA.106.062429","article-title":"Entanglement and coherence in the Bernstein-Vazirani algorithm","volume":"106","author":"Naseri","year":"2022","journal-title":"Phys. Rev. A"},{"issue":"2","key":"10.1016\/j.jlamp.2025.101108_bib0010","doi-asserted-by":"crossref","first-page":"390","DOI":"10.51594\/csitrj.v5i2.790","article-title":"Quantum cryptography and US digital security: a comprehensive review: investigating the potential of quantum technologies in creating unbreakable encryption and their future in national security","volume":"5","author":"Sonko","year":"2024","journal-title":"Comput. Sci. IT Res. J."},{"issue":"1","key":"10.1016\/j.jlamp.2025.101108_bib0011","doi-asserted-by":"crossref","first-page":"2631","DOI":"10.1038\/s41467-021-22539-9","article-title":"Power of data in quantum machine learning","volume":"12","author":"Huang","year":"2021","journal-title":"Nat. Commun."},{"issue":"6","key":"10.1016\/j.jlamp.2025.101108_bib0012","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/s11128-023-03978-3","article-title":"A generalization of Bernstein\u2013Vazirani algorithm with multiple secret keys and a probabilistic oracle","volume":"22","author":"Shukla","year":"2023","journal-title":"Quantum Inf. Process."},{"key":"10.1016\/j.jlamp.2025.101108_bib0013","series-title":"Handbook of Formal Analysis and Verification in Cryptography","first-page":"319","article-title":"Formal methods for quantum algorithms","author":"Chareton","year":"2023"},{"key":"10.1016\/j.jlamp.2025.101108_bib0014","series-title":"Quantum Software (QSW)","first-page":"125","article-title":"Automated verification of Silq quantum programs using SMT solvers","author":"Lewis","year":"2024"},{"key":"10.1016\/j.jlamp.2025.101108_bib0015","series-title":"Tools and Algorithms for the Construction and Analysis of Systems","first-page":"21","article-title":"Verifying quantum communication protocols with ground bisimulation","author":"Qin","year":"2020"},{"key":"10.1016\/j.jlamp.2025.101108_bib0016","series-title":"Encyclopedia of Information Science and Technology, Third Edition","first-page":"7162","article-title":"Formal verification methods","author":"Hasan","year":"2015"},{"issue":"5","key":"10.1016\/j.jlamp.2025.101108_bib0017","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1007\/s10817-020-09584-7","article-title":"Certified quantum computation in Isabelle\/HOL","volume":"65","author":"Bordg","year":"2021","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.jlamp.2025.101108_bib0018","series-title":"Computer Aided Verification","first-page":"187","article-title":"Formal verification of quantum algorithms using quantum Hoare logic","author":"Liu","year":"2019"},{"key":"10.1016\/j.jlamp.2025.101108_bib0019","series-title":"Tools and Algorithms for the Construction and Analysis of Systems","first-page":"363","article-title":"A parallel and distributed quantum SAT solver based on entanglement and teleportation","author":"Lin","year":"2024"},{"key":"10.1016\/j.jlamp.2025.101108_bib0020","series-title":"Programming Languages and Systems: 30th European Symposium on Programming","first-page":"148","article-title":"An automated deductive verification framework for circuit-building quantum programs","author":"Chareton","year":"2021"},{"key":"10.1016\/j.jlamp.2025.101108_bib0021","series-title":"12Th International Conference on Interactive Theorem Proving (ITP 2021)","article-title":"Proving quantum programs correct","author":"Hietala","year":"2021"},{"key":"10.1016\/j.jlamp.2025.101108_bib0022","doi-asserted-by":"crossref","first-page":"1291","DOI":"10.1007\/s11390-021-1637-9","article-title":"Symbolic reasoning about quantum circuits in Coq","volume":"36","author":"Shi","year":"2021","journal-title":"J. Comput. Sci. Technol."},{"key":"10.1016\/j.jlamp.2025.101108_bib0023","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1016\/j.micpro.2019.02.005","article-title":"Formal constraint-based compilation for noisy intermediate-scale quantum systems","volume":"66","author":"Murali","year":"2019","journal-title":"Microprocess. Microsyst."},{"key":"10.1016\/j.jlamp.2025.101108_bib0024","doi-asserted-by":"crossref","first-page":"2086","DOI":"10.1007\/s10773-017-3352-4","article-title":"Quantum cryptography, quantum communication, and quantum computer in a noisy environment","volume":"56","author":"Nagata","year":"2017","journal-title":"Int. J. Theor. Phys. (Dordr)"},{"issue":"2","key":"10.1016\/j.jlamp.2025.101108_bib0025","first-page":"31","article-title":"Implementation of the Bernstein-Vazirani quantum algorithm using the Qiskit framework","volume":"67","author":"Tudorache","year":"2021","journal-title":"Bull. Polytech. Inst. Ia\u0218i, Electr. Eng. Power Eng. Electron. Sect."}],"container-title":["Journal of Logical and Algebraic Methods in Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220825000744?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220825000744?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T04:32:05Z","timestamp":1772598725000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2352220825000744"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3]]},"references-count":25,"alternative-id":["S2352220825000744"],"URL":"https:\/\/doi.org\/10.1016\/j.jlamp.2025.101108","relation":{},"ISSN":["2352-2208"],"issn-type":[{"value":"2352-2208","type":"print"}],"subject":[],"published":{"date-parts":[[2026,3]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Formal reasoning about Bernstein-Vazirani algorithm","name":"articletitle","label":"Article Title"},{"value":"Journal of Logical and Algebraic Methods in Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jlamp.2025.101108","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2025 Elsevier Inc. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"101108"}}