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 条
  • [1] AUTOMATIC VERIFICATION OF FUNCTIONAL PROGRAMS
    DROBUSHEVICH, GA
    ZUBOVICH, KA
    [J]. CYBERNETICS, 1990, 26 (04): : 491 - 502
  • [2] AN EXPERIMENT IN AUTOMATIC VERIFICATION OF PROGRAMS
    WEINBERG, GM
    GRESSETT, GL
    [J]. COMMUNICATIONS OF THE ACM, 1963, 6 (10) : 610 - 613
  • [3] Automatic verification of functional programs
    Drobushevich, G.A.
    Zubovich, K.A.
    [J]. Cybernetics (English Translation of Kibernetika), 1991, 26 (04):
  • [4] Verification of Distributed Quantum Programs
    Feng, Yuan
    Li, Sanjiang
    Ying, Mingsheng
    [J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2022, 23 (03)
  • [5] t Verification of quantum programs
    Ying, Mingsheng
    Yu, Nengkun
    Feng, Yuan
    Duan, Runyao
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2013, 78 (09) : 1679 - 1700
  • [6] Automatic verification of concurrent Ada programs
    Bruneton, E
    Pradat-Peyre, JF
    [J]. RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE' 99, 1999, 1622 : 146 - 157
  • [7] Automatic Verification of Time Behavior of Programs
    Liva, Giovanni
    [J]. PROCEEDINGS 2018 IEEE/ACM 40TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING - COMPANION (ICSE-COMPANION, 2018, : 468 - 471
  • [8] Automatic Verification of Integer Array Programs
    Bozga, Marius
    Habermehl, Peter
    Iosif, Radu
    Konecny, Filip
    Vojnar, Tomas
    [J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2009, 5643 : 157 - +
  • [9] Automatic Verification of Dafny Programs with Traits
    Ahmadi, Reza
    Leino, K. Rustan M.
    Nummenmaa, Jyrki
    [J]. 17TH WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTFJP 2015), 2015,
  • [10] Automatic Verification of Determinism for Structured Parallel Programs
    Vechev, Martin
    Yahav, Eran
    Raman, Raghavan
    Sarkar, Vivek
    [J]. STATIC ANALYSIS, 2010, 6337 : 455 - 471
12345