SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 11:20 - 11:40 at SPLASH-I - R-3 Chair(s): Marieke Huisman, Michael Coblenz
Thu 19 Nov 2020 23:20 - 23:40 at SPLASH-I - R-3 Chair(s): Pranav Kant, Xiangzhe Xu

In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measurements rather than a large number of repeated executions. On the theory side, we rigorously prove that checking projection-based assertions can help locate bugs or statistically assure that the semantic function of the tested program is close to what we expect, for both exact and approximate quantum programs. On the practice side, we consider hardware constraints and introduce several techniques to transform the assertions, making them directly executable on the measurement-restricted quantum computers. We also propose to achieve simplified assertion implementation using local projection technique with soundness guaranteed. We compare Proq with existing quantum program assertions and demonstrate the effectiveness and efficiency of Proq by its applications to assert two sophisticated quantum algorithms, the Harrow-Hassidim-Lloyd algorithm and Shor’s algorithm.

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

11:00 - 12:20: R-3OOPSLA at SPLASH-I +12h
Chair(s): Marieke HuismanUniversity of Twente, Michael CoblenzUniversity of Maryland at College Park
11:00 - 11:20
Talk
OOPSLA
Guannan WeiPurdue University, Oliver BračevacPurdue University, Shangyin TanPurdue University, Tiark RompfPurdue University
Link to publication DOI Pre-print Media Attached
11:20 - 11:40
Talk
OOPSLA
Gushu LiUniversity of California at Santa Barbara, Li ZhouMax Planck Institute for Security and Privacy, Nengkun YuUniversity of Technology Sydney, Yufei DingUniversity of California at Santa Barbara, Mingsheng YingUniversity of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan XieUniversity of California at Santa Barbara
Link to publication DOI Pre-print Media Attached
11:40 - 12:00
Talk
OOPSLA
Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine
Link to publication DOI Media Attached
12:00 - 12:20
Talk
OOPSLA
Cormac FlanaganUniversity of California at Santa Cruz, Stephen N. FreundWilliams College
Link to publication DOI Media Attached
23:00 - 00:20: R-3OOPSLA at SPLASH-I
Chair(s): Pranav KantUniversity of Utah, Xiangzhe XuNanjing University
23:00 - 23:20
Talk
OOPSLA
Guannan WeiPurdue University, Oliver BračevacPurdue University, Shangyin TanPurdue University, Tiark RompfPurdue University
Link to publication DOI Pre-print Media Attached
23:20 - 23:40
Talk
OOPSLA
Gushu LiUniversity of California at Santa Barbara, Li ZhouMax Planck Institute for Security and Privacy, Nengkun YuUniversity of Technology Sydney, Yufei DingUniversity of California at Santa Barbara, Mingsheng YingUniversity of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan XieUniversity of California at Santa Barbara
Link to publication DOI Pre-print Media Attached
23:40 - 00:00
Talk
OOPSLA
Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine
Link to publication DOI Media Attached
00:00 - 00:20
Talk
OOPSLA
Cormac FlanaganUniversity of California at Santa Cruz, Stephen N. FreundWilliams College
Link to publication DOI Media Attached