{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T17:15:49Z","timestamp":1779902149093,"version":"3.53.1"},"reference-count":113,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,12,16]],"date-time":"2023-12-16T00:00:00Z","timestamp":1702684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/T517914\/1"],"award-info":[{"award-number":["EP\/T517914\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Quantum Comput."],"published-print":{"date-parts":[[2024,3,31]]},"abstract":"<jats:p>Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, quantum computers are growing in size rapidly backed up by the increase of research in the field. Significant efforts are being made to improve the reliability of quantum hardware and to develop suitable software to program quantum computers.<\/jats:p>\n          <jats:p>In contrast, the verification of quantum programs has received relatively less attention. Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware. Research into creating verification frameworks for quantum programs has seen recent development, with a variety of tools implemented using a collection of theoretical ideas.<\/jats:p>\n          <jats:p>This survey aims to be a short introduction into the area of formal verification of quantum programs, bringing together theory and tools developed to date. Further, this survey examines some of the challenges that the field may face in the future, namely the development of complex quantum algorithms.<\/jats:p>","DOI":"10.1145\/3624483","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T21:28:08Z","timestamp":1697491688000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Formal Verification of Quantum Programs: Theory, Tools, and Challenges"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4893-7658","authenticated-orcid":false,"given":"Marco","family":"Lewis","sequence":"first","affiliation":[{"name":"Newcastle University, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1922-6678","authenticated-orcid":false,"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[{"name":"Newcastle University, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6033-5919","authenticated-orcid":false,"given":"Paolo","family":"Zuliani","sequence":"additional","affiliation":[{"name":"Newcastle University, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,12,16]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.2573505"},{"key":"e_1_3_4_3_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799359385"},{"key":"e_1_3_4_4_2","volume-title":"Formal Methods in Quantum Circuit Design","author":"Amy Matthew","year":"2019","unstructured":"Matthew Amy. 2019. Formal Methods in Quantum Circuit Design. Ph.D. Dissertation. University of Waterloo. Retrieved from http:\/\/hdl.handle.net\/10012\/14480"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.4204\/Eptcs.287.1"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40578-0_16"},{"key":"e_1_3_4_7_2","first-page":"113","volume-title":"Proceedings of the New Frontiers in Quantitative Methods in Informatics.","author":"Anticoli Linda","year":"2018","unstructured":"Linda Anticoli, Carla Piazza, Leonardo Taglialegne, and Paolo Zuliani. 2018. \\(\\texttt {Entang{$\\lambda$}e}\\) : A translation framework from quipper programs to quantum Markov Chains. In Proceedings of the New Frontiers in Quantitative Methods in Informatics. Simonetta Balsamo, Andrea Marin, and Enrico Vicario (Eds.), Springer International Publishing, Cham, 113\u2013126."},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3231597"},{"key":"e_1_3_4_9_2","unstructured":"Nature"},{"key":"e_1_3_4_10_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.236.1"},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1142\/s0219749908003530"},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484567"},{"key":"e_1_3_4_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_4_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020949"},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.05.025"},{"key":"e_1_3_4_16_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_3_4_17_2","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2013","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer Science & Business Media."},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-019-09302-6"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_3_4_20_2","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_3_4_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-020-09584-7"},{"key":"e_1_3_4_22_2","article-title":"Isabelle marries dirac: A library for quantum computation and quantum information","author":"Bordg Anthony","year":"2020","unstructured":"Anthony Bordg, Hanna Lachnitt, and Yijun He. 2020. Isabelle marries dirac: A library for quantum computation and quantum information. Archive of Formal Proofs (2020). Retrieved from https:\/\/isa-afp.org\/entries\/Isabelle_Marries_Dirac.html, Formal proof development.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_4_23_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.116.250501"},{"key":"e_1_3_4_24_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.aar3106"},{"key":"e_1_3_4_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"e_1_3_4_26_2","doi-asserted-by":"publisher","DOI":"10.1021\/acs.chemrev.8b00803"},{"key":"e_1_3_4_27_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.343.10"},{"key":"e_1_3_4_28_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.MFCS.2019.55"},{"key":"e_1_3_4_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-52869-8.50011-6"},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_4_31_2","doi-asserted-by":"publisher","DOI":"10.1201\/9781003090052-7"},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/QCE53715.2022.00082"},{"key":"e_1_3_4_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/780542.780552"},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_4_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_4_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774"},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_3_4_38_2","volume-title":"Model Checking","author":"Clarke Edmund M","year":"1999","unstructured":"Edmund M Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, London, Cambridge."},{"key":"e_1_3_4_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"e_1_3_4_40_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.23.880"},{"key":"e_1_3_4_41_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_3_4_42_2","unstructured":"Andrea Colledan and Ugo Dal Lago. 2022. On dynamic lifting and effect typing in circuit description languages (Extended Version). arXiv:2202.07636 [cs.PL]."},{"key":"e_1_3_4_43_2","volume-title":"Proceedings of the SMT Workshop: International Workshop on Satisfiability Modulo Theories","author":"Conchon Sylvain","year":"2018","unstructured":"Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. 2018. Alt-Ergo 2.2. In Proceedings of the SMT Workshop: International Workshop on Satisfiability Modulo Theories. Oxford, United Kingdom. Retrieved from https:\/\/hal.inria.fr\/hal-01960203"},{"issue":"1","key":"e_1_3_4_44_2","first-page":"73","article-title":"Model checking for communicating quantum processes","volume":"8","author":"Davidson Timothy A. S.","year":"2012","unstructured":"Timothy A. S. Davidson, Simon J. Gay, Hynek Mlnarik, Rajagopal Nagarajan, and Nick Papanikolaou. 2012. Model checking for communicating quantum processes. Int. J. Unconv. Comput. 8, 1 (2012), 73\u201398. Retrieved from http:\/\/www.oldcitypublishing.com\/journals\/ijuc-home\/ijuc-issue-contents\/ijuc-volume-8-number-1-2012\/ijuc-8-1-p-73-98\/","journal-title":"Int. J. Unconv. Comput."},{"key":"e_1_3_4_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_4_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_3"},{"key":"e_1_3_4_47_2","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.1992.0167"},{"key":"e_1_3_4_48_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_4_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_4_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_4_51_2","article-title":"Quantum projective measurements and the CHSH inequality","author":"Echenim Mnacho","year":"2021","unstructured":"Mnacho Echenim. 2021. Quantum projective measurements and the CHSH inequality. Archive of Formal Proofs (March 2021). Retrieved from https:\/\/isa-afp.org\/entries\/Projective_Measurements.html, Formal proof development.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_4_52_2","unstructured":"Mnacho Echenim and Mehdi Mhalla. 2021. Quantum projective measurements and the CHSH inequality in Isabelle\/HOL. arXiv:2103.08535 [cs.LO]."},{"key":"e_1_3_4_53_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2017.35"},{"key":"e_1_3_4_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_17"},{"key":"e_1_3_4_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_4_56_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2013.04.002"},{"key":"e_1_3_4_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_3_4_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571204"},{"key":"e_1_3_4_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_3_4_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040318"},{"key":"e_1_3_4_61_2","unstructured":"Daniel Gottesman. 1998. The Heisenberg representation of quantum computers. Retrieved January 17 2022 from https:\/\/www.osti.gov\/biblio\/319738"},{"key":"e_1_3_4_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462177"},{"key":"e_1_3_4_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_3_4_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"e_1_3_4_65_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_3_4_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00633-z"},{"key":"e_1_3_4_67_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.21"},{"key":"e_1_3_4_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_4_69_2","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann Gerard","year":"2011","unstructured":"Gerard Holzmann. 2011. The SPIN Model Checker: Primer and Reference Manual (1st. ed.). Addison-Wesley Professional."},{"key":"e_1_3_4_70_2","doi-asserted-by":"publisher","DOI":"10.1145\/3387940.3391459"},{"key":"e_1_3_4_71_2","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.PLATEAU.2018.4"},{"key":"e_1_3_4_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_3_4_73_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.318.14"},{"key":"e_1_3_4_74_2","doi-asserted-by":"publisher","DOI":"10.2172\/366453"},{"key":"e_1_3_4_75_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1997.646094"},{"key":"e_1_3_4_76_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_3_4_77_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_4_78_2","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950600524X"},{"key":"e_1_3_4_79_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_12"},{"key":"e_1_3_4_80_2","article-title":"Quantum hoare logic","author":"Liu Junyi","year":"2019","unstructured":"Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. 2019. Quantum hoare logic. Archive of Formal Proofs (2019). Retrieved from https:\/\/isa-afp.org\/entries\/QHLProver.html, Formal proof development.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_4_81_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139193313.011"},{"key":"e_1_3_4_82_2","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"key":"e_1_3_4_83_2","doi-asserted-by":"publisher","DOI":"10.5555\/1972505"},{"key":"e_1_3_4_84_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63724-2_4"},{"key":"e_1_3_4_85_2","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2747911"},{"key":"e_1_3_4_86_2","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009894"},{"key":"e_1_3_4_87_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_4_88_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_3_4_89_2","doi-asserted-by":"publisher","DOI":"10.1080\/00107514.2019.1667078"},{"key":"e_1_3_4_90_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722010_6"},{"key":"e_1_3_4_91_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_4_92_2","doi-asserted-by":"publisher","DOI":"10.5555\/865018"},{"key":"e_1_3_4_93_2","unstructured":"Yunong Shi Runzhou Tao Xupeng Li Ali Javadi-Abhari Andrew W. Cross Frederic T. Chong and Ronghui Gu. 2020. CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler. (2020). arXiv:1908.08963. Retrieved from https:\/\/arxiv.org\/abs\/1908.08963"},{"key":"e_1_3_4_94_2","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728625"},{"key":"e_1_3_4_95_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795293172"},{"key":"e_1_3_4_96_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_3_4_97_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586191"},{"key":"e_1_3_4_98_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_4_99_2","unstructured":"John van de Wetering. 2020. ZX-calculus for the working quantum computer scientist. arXiv:2012.13966 [quant-ph]."},{"key":"e_1_3_4_100_2","volume-title":"Informal Proceedings of the Workshop on Programming Languages and Quantum Computing","author":"Voichick Finn","year":"2021","unstructured":"Finn Voichick and Michael Hicks. 2021. Toward a quantum programming language for higher-level formal verification. In Informal Proceedings of the Workshop on Programming Languages and Quantum Computing."},{"key":"e_1_3_4_101_2","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530481"},{"key":"e_1_3_4_102_2","doi-asserted-by":"publisher","DOI":"10.1080\/00268976.2011.552441"},{"key":"e_1_3_4_103_2","doi-asserted-by":"publisher","DOI":"10.1007\/11542384"},{"key":"e_1_3_4_104_2","doi-asserted-by":"publisher","DOI":"10.1145\/3491246"},{"key":"e_1_3_4_105_2","doi-asserted-by":"publisher","DOI":"10.1038\/299802a0"},{"key":"e_1_3_4_106_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2022.08.016"},{"key":"e_1_3_4_107_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_4_108_2","unstructured":"Mingsheng Ying and Yuan Feng. 2018. Model Checking Quantum Systems \u2014 A Survey. (2018). arXiv:1807.09466. Retrieved from https:\/\/arxiv.org\/abs\/1807.09466"},{"key":"e_1_3_4_109_2","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507249"},{"key":"e_1_3_4_110_2","unstructured":"Nengkun Yu. 2019. Quantum Temporal Logic. (2019). arXiv:1908.00158. Retrieved from https:\/\/arxiv.org\/abs\/1908.00158"},{"key":"e_1_3_4_111_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498691"},{"key":"e_1_3_4_112_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.abe8770"},{"key":"e_1_3_4_113_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"e_1_3_4_114_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scib.2021.10.017"}],"container-title":["ACM Transactions on Quantum Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3624483","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3624483","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:46Z","timestamp":1750268986000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3624483"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,16]]},"references-count":113,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3,31]]}},"alternative-id":["10.1145\/3624483"],"URL":"https:\/\/doi.org\/10.1145\/3624483","relation":{},"ISSN":["2643-6809","2643-6817"],"issn-type":[{"value":"2643-6809","type":"print"},{"value":"2643-6817","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,16]]},"assertion":[{"value":"2021-10-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-08-24","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-12-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}