Toward automatic verification of quantum programs

被引：16
作者：
Ying, Mingsheng [1 ,2 ,3 ]
机构：
[1] Univ Technol Sydney, Ctr Quantum Software & Informat, Sydney, NSW 2007, Australia
[2] Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China
[3] Tsinghua Univ, Dept Comp Sci & Technol, Beijing, Peoples R China
来源：
FORMAL ASPECTS OF COMPUTING | 2019年 / 31卷 / 01期
基金：
澳大利亚研究理事会;
关键词：
Quantum programming; Hoare logic; Proof outline; Auxiliary rules; Invariant generation; Termination analysis; LINEAR-INVARIANT GENERATION; MODEL CHECKER; TERMINATION; LOGIC;
D O I：
10.1007/s00165-018-0465-3
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：3 / 25
页数：23
相关论文
共 60 条
  • [1] Altenkirch T, 2005, IEEE S LOG, P249
  • [2] Ambainis Andris, 2001, P 33 ACM S THEOR COM, P37, DOI [10.1145/380752.380757, 10.1145/380752.380757.]
  • [3] [Anonymous], 2014, ARXIV14024467
  • [4] Apt K.R., 2009, Texts in Computer Science
  • [5] Ardeshir-Larijani E., 2014, PROC INT C TOOLS ALG, P500
  • [6] LQP: the dynamic logic of quantum information
    Baltag, Alexandru
    Smets, Sonja
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2006, 16 (03) : 491 - 525
  • [7] Probabilistic Relational Verification for Cryptographic Implementations
    Barthe, Gilles
    Fournet, Cedric
    Gregoire, Benjamin
    Strub, Pierre-Yves
    Swamy, Nikhil
    Zanella-Beguelin, Santiago
    [J]. ACM SIGPLAN NOTICES, 2014, 49 (01) : 193 - 205
  • [8] Probabilistic Relational Reasoning for Differential Privacy
    Barthe, Gilles
    Koepf, Boris
    Olmedo, Federico
    Zanella-Beguelin, Santiago
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2013, 35 (03):
  • [9] Dynamic quantum logic for quantum programs
    Brunet, O
    Jorrand, P
    [J]. INTERNATIONAL JOURNAL OF QUANTUM INFORMATION, 2004, 2 (01) : 45 - 54
  • [10] Reasoning About Imperative Quantum Programs
    Chadha, R.
    Mateus, P.
    Sernadas, A.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 158 : 19 - 39
123456