More Web Proxy on the site http://driver.im/

research-article

Verification of Nondeterministic Quantum Programs

Authors:

Yingte XuAuthors Info & Claims

ASPLOS 2023: Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3

Pages 789 - 805

https://doi.org/10.1145/3582016.3582039

Published: 25 March 2023 Publication History

Abstract

Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian operators on the associated Hilbert space. Hoare-type logic systems for partial and total correctness are proposed which turn out to be both sound and relatively complete with respect to their corresponding semantic correctness. To show the utility of these proof systems, we analyse some quantum algorithms such as quantum error correction scheme, Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.

References

[1]

Ralph-Johan Back and Joakim Wright. 2012. Refinement calculus: a systematic introduction. Springer Science & Business Media.

Digital Library

[2]

Yuxin Deng, Yuan Feng, and Ugo Dal Lago. 2015. On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory. 427–440.

[3]

David Deutsch. 1985. Quantum theory, the Church–Turing principle and the universal quantum computer. Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences, 400, 1818 (1985), 97–117.

[4]

Ellie D’Hondt and Prakash Panangaden. 2006. Quantum weakest preconditions. Mathematical Structures in Computer Science, 16, 3 (2006), 429–451.

Digital Library

[5]

Edsger Wybe Dijkstra. 1976. A discipline of programming. Prentice-Hall Englewood Cliffs.

Digital Library

[6]

Yuan Feng, Runyao Duan, Zhengfeng Ji, and Mingsheng Ying. 2007. Proof rules for the correctness of quantum programs. Theoretical Computer Science, 386, 1-2 (2007), 151–166.

Digital Library

[7]

Yuan Feng and Mingsheng Ying. 2021. Quantum Hoare logic with classical variables. ACM Transactions on Quantum Computing, 2, 4 (2021), 1–43.

Digital Library

[8]

Jifeng He, Karen Seidel, and Annabelle McIver. 1997. Probabilistic models for the guarded command language. Science of Computer Programming, 28, 2-3 (1997), 171–192.

[9]

Charles Antony Richard Hoare, He Jifeng, and Augusto Sampaio. 1993. Normal form approach to compiler design. Acta informatica, 30, 8 (1993), 701–739.

[10]

Karl Kraus, Arno Böhm, John D Dollard, and WH Wootters. 1983. States, effects, and operations: fundamental notions of quantum theory. Lecture notes in physics, 190 (1983).

[11]

Yangjia Li and Mingsheng Ying. 2017. Algorithmic analysis of termination problems for quantum programs. In Proceedings of the ACM on Programming Languages. ACM New York, NY, USA, 1–29.

[12]

Yangjia Li, Nengkun Yu, and Mingsheng Ying. 2014. Termination of nondeterministic quantum programs. Acta informatica, 51, 1 (2014), 1–24.

[13]

Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. 2019. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. Springer, Cham, 187–207. https://link.springer.com/chapter/10.1007/978-3-030-25543-5_12

[14]

Annabelle McIver and Carroll Morgan. 2001. Partial correctness for probabilistic demonic programs. Theoretical Computer Science, 266, 1-2 (2001), 09, 513 – 541. https://doi.org/10.1016/s0304-3975(00)00208-5

Digital Library

[15]

Annabelle McIver, Carroll Morgan, and Charles Carroll Morgan. 2005. Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media.

Digital Library

[16]

Graeme Mitchison and Richard Jozsa. 2001. Counterfactual computation. Proceedings of the Royal Society of London. Series A: Mathematical, Physical and Engineering Sciences, 457, 2009 (2001), 1175–1193.

[17]

Carroll Morgan. 1993. The refinement calculus. In Program Design Calculi. Springer, 3–52.

[18]

Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems (TOPLAS), 18, 3 (1996), 325–353.

Digital Library

[19]

Joseph M Morris. 1987. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer programming, 9, 3 (1987), 287–306.

[20]

Michael A Nielsen and Isaac Chuang. 2002. Quantum computation and quantum information. Cambridge University Press.

Digital Library

[21]

Michele Pagani, Peter Selinger, and Benoît Valiron. 2014. Applying quantitative semantics to higher-order quantum computing. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 647–658.

Digital Library

[22]

Jeff W Sanders and Paolo Zuliani. 2000. Quantum programming. In International Conference on Mathematics of Program Construction. 80–99.

[23]

Peter Selinger. 2004. Towards a quantum programming language. Mathematical Structures in Computer Science, 14, 4 (2004), 527–586.

Digital Library

[24]

Peter Selinger and Benoît Valiron. 2006. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16, 3 (2006), 527–552.

Digital Library

[25]

Dominique Unruh. 2019. Quantum relational Hoare logic. Proceedings of the ACM on Programming Languages, 3, POPL (2019), 1–31. https://doi.org/10.1145/3290346

Digital Library

[26]

André Van Tonder. 2004. A lambda calculus for quantum computation. SIAM J. Comput., 33, 5 (2004), 1109–1135.

Digital Library

[27]

John Von Neumann. 1955. Mathematical Foundations of Quantum Mechanics. Princeton University Press, Princeton, NJ.

[28]

Mingsheng Ying. 2012. Floyd–Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 33, 6 (2012), 1–49.

Digital Library

[29]

Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. 2023. CoqQ: Foundational Verification of Quantum Programs. Proceedings of the ACM on Programming Languages, 7, POPL (2023), 833–865.

Digital Library

[30]

Paolo Zuliani. 2004. Non-deterministic quantum programming. In Proceedings of the 2nd International Workshop on Quantum Programming Languages. 179–195.

Cited By

Tan SXiang DLu LLu JJiang QChen MYin JTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident VerificationProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651360(671-688)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651360
Noll TGehnen CHermanns R(2024)Quantum Computing: From Weakest Preconditions to Voltage PulsesPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_9(201-229)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_9

Index Terms

Verification of Nondeterministic Quantum Programs
1. Theory of computation
  1. Logic
    1. Hoare logic
  2. Semantics and reasoning
    1. Program reasoning
    2. Program semantics
      1. Axiomatic semantics
      2. Denotational semantics

Recommendations

Verification of Distributed Quantum Programs
Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of quantum computation. This is particularly true given that developing a general-purpose quantum computer is much more ...
Local Reasoning About Probabilistic Behaviour for Classical–Quantum Programs
Verification, Model Checking, and Abstract Interpretation
Abstract
Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task ...
Toward automatic verification of quantum programs
Abstract
This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASPLOS 2023: Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3

March 2023

820 pages

ISBN:9781450399180

DOI:10.1145/3582016

General Chair:
Tor M. Aamodt
University of British Columbia, Canada
,
Program Chairs:
Natalie Enright Jerger
University of Toronto, Canada
,
Michael Swift
University of Wisconsin-Madison, USA

Copyright © 2023 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

In-Cooperation

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 March 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Australian Research Council

Conference

ASPLOS '23

Sponsor:

ASPLOS '23: 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3

March 25 - 29, 2023

BC, Vancouver, Canada

Acceptance Rates

Overall Acceptance Rate 535 of 2,713 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
241
Total Downloads

Downloads (Last 12 months)88
Downloads (Last 6 weeks)10

Reflects downloads up to 16 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tan SXiang DLu LLu JJiang QChen MYin JTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident VerificationProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651360(671-688)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651360
Noll TGehnen CHermanns R(2024)Quantum Computing: From Weakest Preconditions to Voltage PulsesPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_9(201-229)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_9

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents