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): Michael Coblenz, Marieke Huisman
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

Displayed time zone: Central Time (US & Canada) change

11:00 - 12:20
R-3OOPSLA at SPLASH-I +12h
Chair(s): Michael Coblenz University of Maryland at College Park, Marieke Huisman University of Twente
11:00
20m
Talk
Compiling Symbolic Execution with Staging and Algebraic Effects
OOPSLA
Guannan Wei Purdue University, Oliver Bračevac Purdue University, Shangyin Tan Purdue University, Tiark Rompf Purdue University
Link to publication DOI Pre-print Media Attached
11:20
20m
Talk
Projection-Based Runtime Assertions for Testing and Debugging Quantum ProgramsDistinguished Paper
OOPSLA
Gushu Li University of California at Santa Barbara, Li Zhou Max Planck Institute for Security and Privacy, Nengkun Yu University of Technology Sydney, Yufei Ding University of California at Santa Barbara, Mingsheng Ying University of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan Xie University of California at Santa Barbara
Link to publication DOI Pre-print Media Attached
11:40
20m
Talk
Satune: Synthesizing Efficient SAT Encoders
OOPSLA
Hamed Gorjiara University of California at Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California at Irvine
Link to publication DOI Media Attached
12:00
20m
Talk
The Anchor Verifier for Blocking and Non-blocking Concurrent Software
OOPSLA
Cormac Flanagan University of California at Santa Cruz, Stephen N. Freund Williams College
Link to publication DOI Media Attached
23:00 - 00:20
R-3OOPSLA at SPLASH-I
Chair(s): Pranav Kant University of Utah, Xiangzhe Xu Nanjing University
23:00
20m
Talk
Compiling Symbolic Execution with Staging and Algebraic Effects
OOPSLA
Guannan Wei Purdue University, Oliver Bračevac Purdue University, Shangyin Tan Purdue University, Tiark Rompf Purdue University
Link to publication DOI Pre-print Media Attached
23:20
20m
Talk
Projection-Based Runtime Assertions for Testing and Debugging Quantum ProgramsDistinguished Paper
OOPSLA
Gushu Li University of California at Santa Barbara, Li Zhou Max Planck Institute for Security and Privacy, Nengkun Yu University of Technology Sydney, Yufei Ding University of California at Santa Barbara, Mingsheng Ying University of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan Xie University of California at Santa Barbara
Link to publication DOI Pre-print Media Attached
23:40
20m
Talk
Satune: Synthesizing Efficient SAT Encoders
OOPSLA
Hamed Gorjiara University of California at Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California at Irvine
Link to publication DOI Media Attached
00:00
20m
Talk
The Anchor Verifier for Blocking and Non-blocking Concurrent Software
OOPSLA
Cormac Flanagan University of California at Santa Cruz, Stephen N. Freund Williams College
Link to publication DOI Media Attached