In quantum computing, the basic unit of information is a qubit. Simulation of a general quantum program takes exponential time in the number of qubits, which makes simulation infeasible beyond 50 qubits on current supercomputers. So, for the understanding of larger programs, we turn to static techniques. In this paper, we present an abstract interpretation of quantum programs and we use it to automatically verify assertions in polynomial time. Our key insight is to let an abstract state be a tuple of projections. For such domains, we present abstraction and concretization functions that form a Galois connection and we use them to define abstract operations. Our experiments on a laptop have verified assertions about the Bernstein-Vazirani, GHZ, and Grover benchmarks with 300 qubits.
Thu 16 JunDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 16:50
|(OOPSLA 2020) A Model for Detecting Faults in Build Specifications|
|(OOPSLA 2020) Unifying Execution of Imperative Generators and Declarative Specifications|
|(PLDI 2021) Logical Bytecode Reduction|
|(PLDI 2021) Quantum abstract interpretation|
SIGPLAN TrackLink to publication DOI Authorizer link Pre-print