Document Open Access Logo

Qafny: A Quantum-Program Verifier

Authors Liyi Li , Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.24.pdf
  • Filesize: 0.79 MB
  • 31 pages

Document Identifiers

Author Details

Liyi Li
  • Iowa State University, Ames, IA, USA
Mingwei Zhu
  • University of Maryland, College Park, MD, USA
Rance Cleaveland
  • University of Maryland, College Park, MD, USA
Alexander Nicolellis
  • Iowa State University, Ames, IA, USA
Yi Lee
  • University of Maryland, College Park, MD, USA
Le Chang
  • University of Maryland, College Park, MD, USA
Xiaodi Wu
  • University of Maryland, College Park, MD, USA

Acknowledgements

We thank Finn Voichick for his helpful comments and contributions during the work’s development. This paper is dedicated to the memory of our dear co-author Rance Cleaveland.

Cite AsGet BibTex

Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. Qafny: A Quantum-Program Verifier. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 24:1-24:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.24

Abstract

Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny’s automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover’s algorithm, and Shor’s algorithm.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Quantum information theory
Keywords
  • Quantum Computing
  • Automated Verification
  • Separation Logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. A. Ambainis. Quantum walk algorithm for element distinctness. In 45th Annual IEEE Symposium on Foundations of Computer Science, pages 22-31, 2004. URL: https://doi.org/10.1109/FOCS.2004.54.
  2. Stephane Beauregard. Circuit for shor’s algorithm using 2n+3 qubits. Quantum Info. Comput., 3(2):175-185, March 2003. Google Scholar
  3. Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoît Valiron. An automated deductive verification framework for circuit-building quantum programs. In Nobuko Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 148-177. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_6.
  4. Andrew Childs, Ben Reichardt, Robert Spalek, and Shengyu Zhang. Every NAND formula of size N can be evaluated in time N^1/2+o(1) on a Quantum Computer. CoRR, 2007. URL: https://doi.org//10.48550/arXiv.quant-ph/0703015.
  5. Andrew M. Childs. On the Relationship Between Continuous- and Discrete-Time Quantum Walk. Communications in Mathematical Physics, 294(2):581-603, October 2009. Google Scholar
  6. Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. Vcc: A practical system for verifying concurrent c. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 23-42, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  7. Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. Open quantum assembly language. arXiv e-prints, July 2017. URL: https://arxiv.org/abs/1707.03429.
  8. Paul Adrien Maurice Dirac. A new notation for quantum mechanics. Mathematical Proceedings of the Cambridge Philosophical Society, 35:416-418, 1939. Google Scholar
  9. Mahmudul Faisal Al Ameen and Makoto Tatsuta. Completeness for recursive procedures in separation logic. Theoretical Computer Science, 631:73-96, 2016. URL: https://doi.org/10.1016/j.tcs.2016.04.004.
  10. Yuan Feng and Mingsheng Ying. Quantum hoare logic with classical variables. ACM Transactions on Quantum Computing, 2(4), December 2021. URL: https://doi.org/10.1145/3456877.
  11. Sukhpal Singh Gill, Oktay Cetinkaya, Stefano Marrone, Daniel Claudino, David Haunschild, Leon Schlote, Huaming Wu, Carlo Ottaviani, Xiaoyuan Liu, Sree Pragna Machupalli, Kamalpreet Kaur, Priyansh Arora, Ji Liu, Ahmed Farouk, Houbing Herbert Song, Steve Uhlig, and Kotagiri Ramamohanarao. Quantum computing: Vision and challenges, 2024. URL: https://arxiv.org/abs/2403.02240.
  12. Daniel M. Greenberger, Michael A. Horne, and Anton Zeilinger. Going beyond Bell’s Theorem, pages 69-72. Springer Netherlands, Dordrecht, 1989. URL: https://doi.org/10.1007/978-94-017-0849-4_10.
  13. Lov K. Grover. Quantum mechanics helps in searching for a needle in a haystack. Phys. Rev. Lett., 79:325-328, July 1997. URL: https://doi.org/10.1103/PhysRevLett.79.325.
  14. Thomas Häner, Martin Roetteler, and Krysta M. Svore. Factoring using 2n + 2 qubits with toffoli based modular multiplication. Quantum Info. Comput., 17(7–8):673-684, June 2017. Google Scholar
  15. Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. Proving quantum programs correct. In Proceedings of the Conference on Interative Theorem Proving (ITP), June 2021. Google Scholar
  16. Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for quantum circuits. In Proceedings of the ACM Conference on Principles of Programming Languages (POPL), January 2021. Google Scholar
  17. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, October 1969. URL: https://doi.org/10.1145/363235.363259.
  18. Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey. Cyclic program synthesis. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 944-959, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454087.
  19. Yoshihiko Kakutani. A logic for formal verification of quantum programs. In Anupam Datta, editor, Advances in Computer Science - ASIAN 2009. Information Security and Privacy, pages 79-93, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  20. Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan. A quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498697.
  21. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 348-370, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  22. K. Rustan M. Leino and Michał Moskal. Co-induction simply. In Cliff Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods, pages 382-398, Cham, 2014. Springer International Publishing. Google Scholar
  23. Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, and Michael Hicks. Verified compilation of quantum oracles. In OOPSLA 2022, 2022. URL: https://doi.org/10.48550/arXiv.2112.06700.
  24. Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. Qafny: A quantum-program verifier, 2024. URL: https://arxiv.org/abs/2211.06411.
  25. Yangjia Li and Dominique Unruh. Quantum Relational Hoare Logic with Expectations. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198 of Leibniz International Proceedings in Informatics (LIPIcs), pages 136:1-136:20, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.136.
  26. Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Formal verification of quantum algorithms using quantum hoare logic. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification, pages 187-207, Cham, 2019. Springer International Publishing. Google Scholar
  27. Christof Löding, P. Madhusudan, and Lucas Peña. Foundations for natural proofs and quantifier instantiation. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158098.
  28. Guang Hao Low and Isaac L. Chuang. Optimal Hamiltonian Simulation by Quantum Signal Processing. Physical Review Letters, 118(1), January 2017. Google Scholar
  29. Parthasarathy Madhusudan, Xiaokang Qiu, and Andrei Stefanescu. Recursive proofs for inductive tree data-structures. SIGPLAN Not., 47(1):123-136, January 2012. URL: https://doi.org/10.1145/2103621.2103673.
  30. Frédéric Magniez, Miklos Santha, and Mario Szegedy. Quantum Algorithms for the Triangle Problem. In Proceedings of the Sixteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '05, pages 1109-1117, USA, 2005. Society for Industrial and Applied Mathematics. Google Scholar
  31. Narciso Martí-Oliet and José Meseguer. Rewriting logic as a logical and semantic framework. In J. Meseguer, editor, Electronic Notes in Theoretical Computer Science, volume 4. Elsevier Science Publishers, 2000. Google Scholar
  32. Microsoft. Probabilistic Z3, 2014. URL: https://github.com/ProbabilisticZ3/src.
  33. Yunseong Nam, Neil J. Ross, Yuan Su, Andrew M. Childs, and Dmitri Maslov. Automated optimization of large quantum circuits with continuous parameters. npj Quantum Information, 4(1):23, May 2018. URL: https://doi.org/10.1038/s41534-018-0072-4.
  34. Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, and Daejun Park. Invariant synthesis for incomplete verification engines. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 232-250, Cham, 2018. Springer International Publishing. Google Scholar
  35. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, USA, 10th anniversary edition, 2011. Google Scholar
  36. KARL PEARSON. The problem of the random walk. Nature, 72(1865):294-294, July 1905. URL: https://doi.org/10.1038/072294b0.
  37. Edgar Pek, Xiaokang Qiu, and P. Madhusudan. Natural proofs for data structure manipulation in c using separation logic. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, pages 440-451, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2594291.2594325.
  38. Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, and Xiaodi Wu. A formally certified end-to-end implementation of Shor’s factorization algorithm. Proceedings of the National Academy of Sciences, 120(21):e2218775120, 2023. URL: https://doi.org/10.1073/pnas.2218775120.
  39. Xiaokang Qiu, Pranav Garg, Andrei Ştefănescu, and Parthasarathy Madhusudan. Natural proofs for structure, data, and separation. SIGPLAN Not., 48(6):231-242, June 2013. URL: https://doi.org/10.1145/2499370.2462169.
  40. Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, and Parthasarathy Madhusudan. Natural proofs for structure, data, and separation. In Hans-Juergen Boehm and Cormac Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 231-242. ACM, 2013. URL: https://doi.org/10.1145/2491956.2462169.
  41. Robert Rand. Formally verified quantum programming. PhD thesis, University of Pennsylvania, 2018. Google Scholar
  42. J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 55-74, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  43. Gustavo Rigolin. Quantum teleportation of an arbitrary two-qubit state and its relation to multipartite entanglement. Physical Review A, 71(3), March 2005. URL: https://doi.org/10.1103/physreva.71.032303.
  44. Grigore Roşu and Andrei Ştefănescu. Matching Logic: A New Program Verification Approach (NIER Track). In ICSE'11: Proceedings of the 30th International Conference on Software Engineering, pages 868-871. ACM, 2011. URL: https://doi.org/doi:10.1145/1985793.1985928.
  45. Grigore Roşu, Andrei Ştefănescu, Ştefan Ciobâcă, and Brandon M. Moore. One-Path Reachability Logic. In Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13), pages 358-367. IEEE, June 2013. Google Scholar
  46. Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. Refinedc: Automating the foundational verification of c code with refined ownership types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 158-174, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454036.
  47. P. W. Shor. Algorithms for quantum computation: Discrete logarithms and factoring. In Proceedings 35th Annual Symposium on Foundations of Computer Science, FOCS '94, 1994. Google Scholar
  48. P.W. Shor. Algorithms for quantum computation: discrete logarithms and factoring. In Proceedings 35th Annual Symposium on Foundations of Computer Science, pages 124-134, 1994. URL: https://doi.org/10.1109/SFCS.1994.365700.
  49. Matt Swayne. What Are The Remaining Challenges Of Quantum Computing?, 2023. URL: https://thequantuminsider.com/2023/03/24/quantum-computing-challenges/.
  50. Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. Automated mutual explicit induction proof in separation logic, 2016. URL: https://doi.org/10.48550/arXiv.1609.00919.
  51. Makoto Tatsuta, Wei-Ngan Chin, and Mahmudul Faisal Al Ameen. Completeness and expressiveness of pointer program verification by separation logic. Information and Computation, 267:1-27, 2019. URL: https://doi.org/10.1016/j.ic.2019.03.002.
  52. Dominique Unruh. Quantum relational hoare logic. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290346.
  53. Salvador Elías Venegas-Andraca. Quantum walks: a comprehensive review. Quantum Information Processing, 11(5):1015-1106, July 2012. URL: https://doi.org/10.1007/s11128-012-0432-5.
  54. Thomas G. Wong. Unstructured search by random and quantum walk. Quantum Information and Computation, 22(1&2):53-85, January 2022. URL: https://doi.org/10.26421/qic22.1-2-4.
  55. Hongseok Yang and Peter O'Hearn. A semantic basis for local reasoning. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, pages 402-416, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. Google Scholar
  56. Mingsheng Ying. Floyd-hoare logic for quantum programs. ACM Trans. Program. Lang. Syst., 33(6), January 2012. URL: https://doi.org/10.1145/2049706.2049708.
  57. Mingsheng Ying. Toward automatic verification of quantum programs. Form. Asp. Comput., 31(1):3-25, February 2019. URL: https://doi.org/10.1007/s00165-018-0465-3.
  58. Bohua Zhan. Efficient verification of imperative programs using auto2. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 23-40, Cham, 2018. Springer International Publishing. Google Scholar
  59. Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. A Quantum Interpretation of Bunched Logic and Quantum Separation Logic. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '21, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1109/LICS52264.2021.9470673.
  60. Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. Coqq: Foundational verification of quantum programs. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571222.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact