{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:13Z","timestamp":1740109093927,"version":"3.37.3"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2019,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Quantum computing systems promise to increase the capabilities for solving problems which classical computers cannot handle adequately, such as integers factorization. In this paper, we present a formal modeling and verification approach for optical quantum circuits, where we build a rich library of optical quantum gates and develop a proof strategy in higher-order logic to reason about optical quantum circuits automatically. The constructed library contains a variety of quantum gates ranging from 1-qubit to 3-qubit gates that are sufficient to model most existing quantum circuits. As real world applications, we present the formal analysis of several quantum circuits including quantum full adders and the Grover\u2019s oracle circuits, for which we have proved the behavioral correctness and calculated the operational success rate, which has never been provided in the literature. We show through several case studies the efficiency of the proposed framework in terms of the scalability and modularity.<\/jats:p>","DOI":"10.1007\/s00165-019-00480-5","type":"journal-article","created":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T20:15:08Z","timestamp":1552680908000},"page":"321-351","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A modeling and verification framework for optical quantum circuits"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6526-9295","authenticated-orcid":false,"given":"Sidi Mohamed","family":"Beillahi","sequence":"first","affiliation":[{"name":"Department of Electrical and Computer Engineering, Concordia University, Montreal, QC, Canada"}]},{"given":"Mohamed Yousri","family":"Mahmoud","sequence":"additional","affiliation":[{"name":"Department of Electrical Engineering and Computer Science, University of Ottawa, Ottawa, ON, Canada"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Concordia University, Montreal, QC, Canada"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.52.3457"},{"key":"e_1_2_1_2_2_2","unstructured":"Beillahi SM Mahmoud MY (2019) HOL-light source code. https:\/\/github.com\/beillahi\/FMV-QC-HOL.git"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Beillahi SM Mahmoud MY Tahar S (2016) Hierarchical verification of quantum circuits. In: Proceedings of NASA formal methods (NFM 2016) LNCS 9690. Springer pp 344\u2013352","DOI":"10.1007\/978-3-319-40648-0_26"},{"volume-title":"Optical quantumgates formalization in hol light Technical Report, ECED epartment, Concordia University","year":"2016","author":"Beillahi SM","key":"e_1_2_1_2_4_2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539796300921"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Black PE Lane AW (2004) Modeling quantum information systems. In: Proceedings of quantum information and computation II. SPIE 5436 pp. 340\u2013347","DOI":"10.1117\/12.537667"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Boender J Kamm\u00fcller F Nagarajan R(2015) Formalization of quantum protocols using Coq. In: Proceedings of international workshop on quantum physics and logic (QPL 2015) pp 71\u201383","DOI":"10.4204\/EPTCS.195.6"},{"issue":"1","key":"e_1_2_1_2_8_2","first-page":"23","article-title":"On the theory of superfluidity","volume":"11","author":"Bogoliubov NN","year":"1947","journal-title":"J Phys (USSR)"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.3390\/e12112268"},{"key":"e_1_2_1_2_10_2","unstructured":"Bruce JW Thornton MA Shivakumaraiah L Kokate PS Li X (2002) Efficient adder circuits based on a conservative reversible logic gate. In: Proceedings of IEEE computer society annual symposium on VLSI (ISVLSI 2002) pp 83\u201388"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.5555\/2011827.2011828"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Franke-Arnold S Gay SJ Puthoor IV (2013) Quantum process calculus for linear optical quantum computing. In: Proceedings of reversible computation (RC 2013) LNCS 7948. Springer pp 234\u2013246","DOI":"10.1007\/978-3-642-38986-3_19"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Golubitsky O Falconer SM Maslov D (2010) Synthesis of the optimal 4-bit reversible circuits. In: Proceedings of design automation conference (DAC 2010) pp. 653\u2013656","DOI":"10.1145\/1837274.1837440"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2009.2017215"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"H\u00e4ner T Steiger DS Smelyanskiy M Troyer M (2016) High performance emulation of quantum circuits. In: Proceedings of international conference for high performance computing networking storage and analysis (SC 2016) pp 866\u2013874","DOI":"10.1109\/SC.2016.73"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/1540610"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Harrison J (1996) HOL light: a tutorial introduction. proc. formal methods in computer-aided design (FMCAD1996) LNCS 1166. Springer pp 265\u2013269","DOI":"10.1007\/BFb0031814"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/38.2.162"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.858352"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Hung WNN Song X Yang G Yang J Perkowski MA (2004) Quantum logic synthesis by symbolic reachability analysis. In: Proceedings of design automation conference (DAC 2004) pp 838\u2013841","DOI":"10.1145\/996566.996790"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Khammassi N Ashraf I Fu X Almudever CG Bertels K (2017) QX: a high-performance quantum computer simulation platform. In: Proceedings of design automation and test in Europe (DATE 2017) pp 464\u2013469","DOI":"10.23919\/DATE.2017.7927034"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1103\/RevModPhys.79.135"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1038\/35051009"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Knill EH (1996) Conventions for quantum pseudocode. Technical Report LAUR-96-2724 Los Alamos National Laboratory","DOI":"10.2172\/366453"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.72.024303"},{"key":"e_1_2_1_2_26_2","unstructured":"Liu T Li Y Wang S Mingsheng Y Zhan N (2016) A theorem prover for quantum hoare logic and its applications. CoRR. arXiv:1601.03835"},{"key":"e_1_2_1_2_27_2","unstructured":"Mahmoud MY (2015) Formal analysis of quantum optics. Ph.D. Department of Electrical and Computer Engineering Concordia University Montreal Quebec"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Mahmoud MY Panangaden P Tahar S (2015) On the formal verification of optical quantum gates in HOL. In: Proceedings of formal methods for industrial critical systems (FMICS 2015) LNCS vol 9128. Springer pp 198\u2013211","DOI":"10.1007\/978-3-319-19458-5_13"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Mahmoud MY Aravantinos V Tahar S (2014) Formal verification of optical quantum flip gate. In: Proceedings interactive theorem proving (ITP 2014) LNCS vol 8558. Springer pp 358\u2013373","DOI":"10.1007\/978-3-319-08970-6_23"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"MahmoudMY Aravantinos V Tahar S (2013) Formalization of infinite dimension linear spaces with application to quantum theory. In: Proceedings NASA formal methods (NFM 2013) LNCS vol 7871. Springer pp 413\u2013427","DOI":"10.1007\/978-3-642-38088-4_28"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139644105","volume-title":"Optical coherence and quantum optics","author":"Mandel L","year":"1995"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.62.2124"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2459034"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Niemann P Wille R Drechsler R (2014) Efficient synthesis of quantum circuits implementing Clifford group operations. In: Proceedings of Asia and South Pacific design automation conference (ASP-DAC 2014) pp 483\u2013488","DOI":"10.1109\/ASPDAC.2014.6742938"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1974.11993680"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.1173731"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.75.022313"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.68.042319"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.65.062324"},{"key":"e_1_2_1_2_41_2","unstructured":"RevLib: an online resource for benchmarks within the domain of reversible and quantum circuits. http:\/\/www.revlib.org\/\n 2018."},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Rand R Paykin J Zdancewic S (2018) QWIRE practice: formal verification of quantum verification in Coq. In: Proceedings of international conference on quantum physics and logic (QPL 2017) EPTCS vol 266 pp 119\u201313","DOI":"10.4204\/EPTCS.266.8"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Rand R Paykin J Zdancewic S (2017) QWIRE: a core language for quantum circuits. In: Proceedings of ACM SIGPLAN symposium on principles of programming languages (POPL 2017) ACM pp 846\u2013858","DOI":"10.1145\/3093333.3009894"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Soeken M Wille R Hilken C Przigoda N Drechsler R (2012) Synthesis of reversible circuits with minimal lines for large functions. In: Proceedings of Asia and South Pacific design automation conference (ASP-DAC 2012) pp 85\u201392","DOI":"10.1109\/ASPDAC.2012.6165069"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Sasanian Z Wille R Miller DM (2012) Realizing reversible circuits using a new class of quantum gates. In: Proceedings of design automation conference (DAC 2012) pp 36\u201341","DOI":"10.1145\/2228360.2228368"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.855930"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795293172"},{"key":"e_1_2_1_2_48_2","unstructured":"Smelyanskiy M Sawaya NPD Aspuru-Guzik A (2016) qHiPSTER: the quantum high performance software testing environment. CoRR. arXiv:1601.07195"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Viamontes GF Rajagopalan M Markov IL Hayes JP (2003) Gate level simulation of quantum circuits. In: Proceedings of Asia and South Pacific design automation conference (ASP-DAC 2003) pp 295\u2013301","DOI":"10.1145\/1119772.1119829"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1038\/nphoton.2017.63"},{"key":"e_1_2_1_2_51_2","unstructured":"Wecker D Svore KM(2014) LIQUi \u27e9|: A software design architecture and domain-specific language for quantum computing. CoRR. arXiv:1402.4467"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Wille R Lye A Drechsler R (2014) Optimal SWAP gate insertion for nearest neighbor quantum circuits. In: Proceedings of Asia and South Pacific design automation conference (ASP-DAC 2014) pp 489\u2013494","DOI":"10.1109\/ASPDAC.2014.6742939"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.5555\/2011464.2011465"},{"issue":"6","key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","first-page":"19:1","DOI":"10.1145\/2049706.2049708","article-title":"Floyd\u2013Hoare logic for quantum programs","volume":"33","author":"Ying M","year":"2011","journal-title":"ACM Trans Program Lang Syst"},{"key":"e_1_2_1_2_55_2","unstructured":"Zulehner A Wille R (2017) Advanced simulation of quantum computations. CoRR. arXiv:1707.00865"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-019-00480-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-019-00480-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-019-00480-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-019-00480-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:56:19Z","timestamp":1641538579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-019-00480-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["10.1007\/s00165-019-00480-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-019-00480-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2019,6]]},"assertion":[{"value":"11 January 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 February 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}