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
相关论文
共 50 条
  • [41] Automatic Verification of C and Java']Java Programs: SV-COMP 2019
    Beyer, Dirk
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, 2019, 11429 : 133 - 155
  • [42] Automatic verification of pointer programs using grammar-based shape analysis
    Lee, O
    Yang, HS
    Yi, KK
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2005, 3444 : 124 - 140
  • [43] Automatic verification of pointer programs using monadic second-order logic
    Jensen, JL
    Jorgensen, ME
    Klarlund, N
    Schwartzbach, MI
    [J]. ACM SIGPLAN NOTICES, 1997, 32 (05) : 226 - 234
  • [44] An Automated Deductive Verification Framework for Circuit-building Quantum Programs
    Chareton, Christophe
    Bardin, Sebastien
    Bobot, Francois
    Perrelle, Valentin
    Valiron, Benoit
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2021, 2021, 12648 : 148 - 177
  • [45] Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications
    Le, Xuan-Bach
    Sanan, David
    Jun, Sun
    Lin, Shang-Wei
    [J]. 2020 25TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2020), 2020, : 43 - 52
  • [46] Automatic Verification of Mixed-Signal ATE Test Programs using Device Variation
    Mayer, Franziska
    Schott, Christian
    Billich, Enrico
    Yazdani, Saeid
    Heinkel, Ulrich
    Daler, Georg
    Ruf, Bernhard
    Pannuzzo, Ricardo
    Dickenscheid, Wolfgang
    [J]. 2021 IEEE INTERNATIONAL TEST CONFERENCE (ITC 2021), 2021, : 374 - 379
  • [47] An automatic verification technique for loop and data reuse transformations based on geometric modeling of programs
    Shashidhar, KC
    Bruynooghe, M
    Catthoor, F
    Janssens, G
    [J]. JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2003, 9 (03) : 248 - 269
  • [48] Verification of JCSP Programs
    Klebanov, Vladimir
    Ruemmer, Philipp
    Schlager, Steffen
    Schmitt, Peter H.
    [J]. COMMUNICATION PROCESS ARCHITECTURES 2005, 2005, 63 : 203 - 218
  • [49] VERIFICATION OF SOFTWARE PROGRAMS
    BUCKLEY, FJ
    [J]. COMPUTERS AND AUTOMATION, 1971, 20 (02): : 23 - &
  • [50] On the verification of SCOOP programs
    Caltais, Georgiana
    Meyer, Bertrand
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2017, 133 : 194 - 215
12345