Quantum Abstract Interpretation

Explore quantum abstract interpretation in this conference talk presented by Jens Palsberg at PLDI 2021. Delve into the challenges of simulating quantum programs with large numbers of qubits and discover a novel static technique for program analysis. Learn about the key insight of representing abstract states as tuples of projections, and understand how abstraction and concretization functions form a Galois connection to define abstract operations. Examine the application of this approach to automatically verify assertions in polynomial time, with examples from benchmarks such as Bernstein-Vazirani, GHZ, and Grover involving up to 300 qubits. Gain insights into this joint work with Nengkun Yu, which offers a promising solution for analyzing and understanding large-scale quantum programs beyond the current simulation capabilities of supercomputers.