{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,27]],"date-time":"2026-06-27T03:45:58Z","timestamp":1782531958001,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523431","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"641-656","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["Giallar: push-button verification for the qiskit Quantum compiler"],"prefix":"10.1145","author":[{"given":"Runzhou","family":"Tao","sequence":"first","affiliation":[{"name":"Columbia University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yunong","family":"Shi","sequence":"additional","affiliation":[{"name":"Amazon, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jianan","family":"Yao","sequence":"additional","affiliation":[{"name":"Columbia University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xupeng","family":"Li","sequence":"additional","affiliation":[{"name":"Columbia University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ali","family":"Javadi-Abhari","sequence":"additional","affiliation":[{"name":"IBM Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew W.","family":"Cross","sequence":"additional","affiliation":[{"name":"IBM Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frederic T.","family":"Chong","sequence":"additional","affiliation":[{"name":"University of Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[{"name":"Columbia University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_1"},{"key":"e_1_3_2_1_3_1","unstructured":"Juan Carlos Garcia-Escartin and Pedro Chamorro-Posada. 2011. Equivalent Quantum Circuits. Universidad de Valladolid Dpto. Teoria de la Senal e Ing.. arxiv:1110.2998v1.  Juan Carlos Garcia-Escartin and Pedro Chamorro-Posada. 2011. Equivalent Quantum Circuits. Universidad de Valladolid Dpto. Teoria de la Senal e Ing.. arxiv:1110.2998v1."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_2_1_5_1","unstructured":"The Coq Development Team. 2012. The Coq Reference Manual version 8.4. Available electronically at http:\/\/coq.inria.fr\/doc  The Coq Development Team. 2012. The Coq Reference Manual version 8.4. Available electronically at http:\/\/coq.inria.fr\/doc"},{"key":"e_1_3_2_1_6_1","unstructured":"Andrew W Cross Lev S Bishop John A Smolin and Jay M Gambetta. 2017. Open quantum assembly language. arxiv:1707.03429.  Andrew W Cross Lev S Bishop John A Smolin and Jay M Gambetta. 2017. Open quantum assembly language. arxiv:1707.03429."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_7"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9780511607219"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0849-4_10"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676975"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192381"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428289"},{"key":"e_1_3_2_1_14_1","unstructured":"Thomas H\u00e4ner Torsten Hoefler and Matthias Troyer. 2018. Using Hoare Logic for Quantum Circuit Optimization. arxiv:1810.00375.  Thomas H\u00e4ner Torsten Hoefler and Matthias Troyer. 2018. Using Hoare Logic for Quantum Circuit Optimization. arxiv:1810.00375."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_3_2_1_18_1","volume-title":"LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. UIUC","author":"Lattner Chris","year":"2003","unstructured":"Chris Lattner and Vikram Adve . 2003 . LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. UIUC . http:\/\/llvm.cs.uiuc.edu\/ Chris Lattner and Vikram Adve. 2003. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. UIUC. http:\/\/llvm.cs.uiuc.edu\/"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_20_1","unstructured":"Ang Li Samuel Stein Sriram Krishnamoorthy and James Ang. 2021. QASMBench: A Low-level QASM Benchmark Suite for NISQ Evaluation and Simulation. arxiv:2005.13018.  Ang Li Samuel Stein Sriram Krishnamoorthy and James Ang. 2021. QASMBench: A Low-level QASM Benchmark Suite for NISQ Evaluation and Simulation. arxiv:2005.13018."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304023"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01461-2_8"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2007.911334"},{"key":"e_1_3_2_1_25_1","volume-title":"Gambetta","author":"McKay David C.","year":"2018","unstructured":"David C. McKay , Thomas Alexander , Luciano Bello , Michael J. Biercuk , Lev Bishop , Jiayin Chen , Jerry M. Chow , Antonio D. C\u00f3rcoles , Daniel Egger , Stefan Filipp , Juan Gomez , Michael Hush , Ali Javadi-Abhari , Diego Moreda , Paul Nation , Brent Paulovicks , Erick Winston , Christopher J. Wood , James Wootton , and Jay M . Gambetta . 2018 . Qiskit Backend Specifications for OpenQASM and OpenPulse Experiments . arxiv:1809.03452. David C. McKay, Thomas Alexander, Luciano Bello, Michael J. Biercuk, Lev Bishop, Jiayin Chen, Jerry M. Chow, Antonio D. C\u00f3rcoles, Daniel Egger, Stefan Filipp, Juan Gomez, Michael Hush, Ali Javadi-Abhari, Diego Moreda, Paul Nation, Brent Paulovicks, Erick Winston, Christopher J. Wood, James Wootton, and Jay M. Gambetta. 2018. Qiskit Backend Specifications for OpenQASM and OpenPulse Experiments. arxiv:1809.03452."},{"key":"e_1_3_2_1_26_1","unstructured":"Microsoft. 2016. F*. https:\/\/github.com\/FStarLang\/FStar\/  Microsoft. 2016. F*. https:\/\/github.com\/FStarLang\/FStar\/"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Frank Mueller Greg Byrd and Patrick Dreher. 2020. Programming Quantum Computers: A Primer with IBM Q and D-Wave Exercises. https:\/\/sites.google.com\/ncsu.edu\/qc-tutorial  Frank Mueller Greg Byrd and Patrick Dreher. 2020. Programming Quantum Computers: A Primer with IBM Q and D-Wave Exercises. https:\/\/sites.google.com\/ncsu.edu\/qc-tutorial","DOI":"10.1145\/3293883.3302578"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304075"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378477"},{"key":"e_1_3_2_1_30_1","volume-title":"Automated Optimization of Large Quantum Circuits with Continuous Parameters. npj Quantum Information, 4, 1","author":"Nam Yunseong","year":"2018","unstructured":"Yunseong Nam , Neil J Ross , Yuan Su , Andrew M Childs , and Dmitri Maslov . 2018. Automated Optimization of Large Quantum Circuits with Continuous Parameters. npj Quantum Information, 4, 1 ( 2018 ), 1\u201312. Yunseong Nam, Neil J Ross, Yuan Su, Andrew M Childs, and Dmitri Maslov. 2018. Automated Optimization of Large Quantum Circuits with Continuous Parameters. npj Quantum Information, 4, 1 (2018), 1\u201312."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_2_1_36_1","unstructured":"2021. Available at https:\/\/qiskit.org\/documentation\/index.htm  2021. Available at https:\/\/qiskit.org\/documentation\/index.htm"},{"key":"e_1_3_2_1_37_1","unstructured":"2019. Available at https:\/\/github.com\/Qiskit\/qiskit-terra\/issues\/1871  2019. Available at https:\/\/github.com\/Qiskit\/qiskit-terra\/issues\/1871"},{"key":"e_1_3_2_1_38_1","unstructured":"2021. Available at https:\/\/github.com\/Qiskit\/qiskit-terra  2021. Available at https:\/\/github.com\/Qiskit\/qiskit-terra"},{"key":"e_1_3_2_1_39_1","unstructured":"2018. Available at https:\/\/github.com\/Qiskit\/qiskit-terra\/issues  2018. Available at https:\/\/github.com\/Qiskit\/qiskit-terra\/issues"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Robert Rand Jennifer Paykin Dong-Ho Lee and Steve Zdancewic. 2019. ReQWIRE: Reasoning about Reversible Quantum Circuits. arxiv:1901.10118.  Robert Rand Jennifer Paykin Dong-Ho Lee and Steve Zdancewic. 2019. ReQWIRE: Reasoning about Reversible Quantum Circuits. arxiv:1901.10118.","DOI":"10.4204\/EPTCS.287.17"},{"key":"e_1_3_2_1_41_1","volume-title":"Proceedings of the 8th International Conference on Learning Representations (ICLR \u201920)","author":"Ryan Gabriel","year":"2020","unstructured":"Gabriel Ryan , Justin Wong , Jianan Yao , Ronghui Gu , and Suman Jana . 2020 . CLN2INV: Learning Loop Invariants with Continuous Logic Networks . In Proceedings of the 8th International Conference on Learning Representations (ICLR \u201920) . https:\/\/openreview.net\/forum?id=HJlfuTEtvB Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. 2020. CLN2INV: Learning Loop Invariants with Continuous Logic Networks. In Proceedings of the 8th International Conference on Learning Representations (ICLR \u201920). https:\/\/openreview.net\/forum?id=HJlfuTEtvB"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304018"},{"key":"e_1_3_2_1_43_1","unstructured":"Yunong Shi Runzhou Tao Xupeng Li Ali Javadi-Abhari Andrew W Cross Frederic T Chong and Ronghui Gu. 2019. CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler. arxiv:1908.08963.  Yunong Shi Runzhou Tao Xupeng Li Ali Javadi-Abhari Andrew W Cross Frederic T Chong and Ronghui Gu. 2019. CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler. arxiv:1908.08963."},{"key":"e_1_3_2_1_44_1","volume-title":"Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201916)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson , James Bornholt , Emina Torlak , and Xi Wang . 2016 . Push-Button Verification of File Systems via Crash Refinement . In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201916) . 1\u201316. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/sigurbjarnarson Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201916). 1\u201316. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/sigurbjarnarson"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454029"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397246"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"},{"key":"e_1_3_2_1_48_1","unstructured":"Vladimir Zamdzhiev. 2016. Quantum Computing: the Good the bad and the (not so) Ugly!. Invited Talk at University of Oxford.  Vladimir Zamdzhiev. 2016. Quantum Computing: the Good the bad and the (not so) Ugly!. Invited Talk at University of Oxford."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE51524.2021.9678908"}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"San Diego CA USA","acronym":"PLDI '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523431","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523431","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:31:16Z","timestamp":1750188676000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523431"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":49,"alternative-id":["10.1145\/3519939.3523431","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523431","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}