Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

ACM SIGPLAN Notices

Invariants of quantum programs: characterisations and generation

Mingsheng Ying, Shenggang Ying, Xiaodi Wu

Published Jan 1, 2017• 18 citations
Publisher

Abstract

Program invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find an appropriate definition of invariants for quantum programs; and (ii) develop an effective technique of invariant generation for verification and analysis of quantum programs. Interestingly, the notion of invariant can be defined for quantum programs in two different ways -- additive invariants and multiplicative invariants -- corresponding to two interpretations of implication in a continuous valued logic: the Lukasiewicz implication and the Godel implication. It is shown that both of them can be used to establish partial correctness of quantum programs. The problem of generating additive invariants of quantum programs is addressed by reducing it to an SDP (Semidefinite Programming) problem. This approach is applied with an SDP solver to generate invariants of two important quantum algorithms -- quantum walk and quantum Metropolis sampling. Our examples show that the generated invariants can be used to verify correctness of these algorithms and are helpful in optimising quantum Metropolis sampling. To our knowledge, this paper is the first attempt to define the notion of invariant and to develop a method of invariant generation for quantum programs.

DOI
10.1145/3093333.3009840

Related papers

Invariants of quantum programs: characterisations and generation

Mingsheng Ying, Shenggang Ying, Xiaodi Wu

Program invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find an appropriate definition of invariants for quantum programs; and (ii) develop an effective technique of invariant generation for verification and analysis of quantum programs.

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)•Dec 22, 2016•34 citations

Toward automatic verification of quantum programs

Mingsheng Ying

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. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.

arXiv:1807.11610•Formal Aspects of Computing•Aug 7, 2018•26 citations

Toward automatic verification of quantum programs

Mingsheng Ying

© 2018, British Computer Society. 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. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.

•Jan 1, 2019•25 citations

Verification of Nondeterministic Quantum Programs

Yuan Feng, Yingte Xu

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.

arXiv:2302.07973•International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)•Mar 20, 2023•11 citations

Semidefinite Programming in Quantum Information Science

Paul Skrzypczyk, Daniel Cavalcanti

Semidefinite programs (SDPs) are a class of optimisation problems that find application in numerous areas of physics, engineering and mathematics. Semidefinite programming is particularly suited to problems in quantum physics and quantum information science. Following a review of the theory of semidefinite programming, the book proceeds to describe how it can be used to address a wide range of important problems from across quantum information science. Specific applications include quantum state, measurement, and channel estimation and discrimination, entanglement detection and quantification, quantum distance measures, and measurement incompatibility. Though SDPs have become an increasingly important tool in quantum information science it’s not yet the kind of mathematics students learn routinely. Assuming only a basic knowledge of linear algebra and quantum physics and quantum information, this graduate-level book provides a unified and accessible presentation of one of the key numerical methods used in quantum information science. Whilst the focus is on the theoretical machinery of SDPs, the authors have provided an accompanying GitHub repository containing example code, covering some of the SDPs studied in this book. Part of IOP Series in Quantum Technology. Key features • Accessible for graduate students in science and mathematics. • A unified and accessible presentation of one of the key numerical methods used in quantum information science. • Written by leading researchers on the topic. • Accompanying GitHub repository with sample code.

arXiv:2306.11637•Institute of Physics eBooks•Mar 1, 2023•64 citations

Verification of Distributed Quantum Programs

Yuan Feng, Sanjiang Li, Mingsheng Ying

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 difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifying their correctness. In this paper, we propose a CSP-like distributed programming language to facilitate the specification and verification of such systems. After presenting its operational and denotational semantics, we develop a Hoare-style logic for distributed quantum programs and establish its soundness and (relative) completeness with respect to both partial and total correctness. The effectiveness of the logic is demonstrated by its applications in the verification of quantum teleportation and local implementation of non-local CNOT gates, two important algorithms widely used in distributed quantum systems.

arXiv:2104.14796•ACM Transactions on Computational Logic•Mar 29, 2022•16 citations
Program invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find an appropriate definition of invariants for quantum programs; and (ii) develop an effective technique of invariant generation for verification and analysis of quantum programs. Interestingly, the notion of invariant can be defined for quantum programs in two different ways -- additive invariants and multiplicative invariants -- corresponding to two interpretations of implication in a continuous valued logic: the Lukasiewicz implication and the Godel implication. It is shown that both of them can be used to establish partial correctness of quantum programs. The problem of generating additive invariants of quantum programs is addressed by reducing it to an SDP (Semidefinite Programming) problem. This approach is applied with an SDP solver to generate invariants of two important quantum algorithms -- quantum walk and quantum Metropolis sampling. Our examples show that the generated invariants can be used to verify correctness of these algorithms and are helpful in optimising quantum Metropolis sampling. To our knowledge, this paper is the first attempt to define the notion of invariant and to develop a method of invariant generation for quantum programs.
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.
Semidefinite programs (SDPs) are a class of optimisation problems that find application in numerous areas of physics, engineering and mathematics. Semidefinite programming is particularly suited to problems in quantum physics and quantum information science. Following a review of the theory of semidefinite programming, the book proceeds to describe how it can be used to address a wide range of important problems from across quantum information science. Specific applications include quantum state, measurement, and channel estimation and discrimination, entanglement detection and quantification, quantum distance measures, and measurement incompatibility. Though SDPs have become an increasingly important tool in quantum information science it’s not yet the kind of mathematics students learn routinely. Assuming only a basic knowledge of linear algebra and quantum physics and quantum information, this graduate-level book provides a unified and accessible presentation of one of the key numerical methods used in quantum information science. Whilst the focus is on the theoretical machinery of SDPs, the authors have provided an accompanying GitHub repository containing example code, covering some of the SDPs studied in this book. Part of IOP Series in Quantum Technology. Key features • Accessible for graduate students in science and mathematics. • A unified and accessible presentation of one of the key numerical methods used in quantum information science. • Written by leading researchers on the topic. • Accompanying GitHub repository with sample code.
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 difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifying their correctness. In this paper, we propose a CSP-like distributed programming language to facilitate the specification and verification of such systems. After presenting its operational and denotational semantics, we develop a Hoare-style logic for distributed quantum programs and establish its soundness and (relative) completeness with respect to both partial and total correctness. The effectiveness of the logic is demonstrated by its applications in the verification of quantum teleportation and local implementation of non-local CNOT gates, two important algorithms widely used in distributed quantum systems.