POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sat 20 Jan 2024 11:00 - 11:45 at Siemens Boardroom - Invited Talks 2 Chair(s): Caterina Urban

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. 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. Joint work with Nengkun Yu. Presented at PLDI 2021.

Sat 20 Jan

Displayed time zone: London change

11:00 - 12:30
Invited Talks 2N40AI at Siemens Boardroom
Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL
Quantum Abstract Interpretation
Jens Palsberg University of California, Los Angeles (UCLA)
Trust but Verify: Scaling Deductive Verification with Abstract Interpretation
Mooly Sagiv Tel Aviv University
File Attached