Bug-catching is important for developing quantum programs. Motivated by the incorrectness logic for classical programs, we propose an incorrectness logic towards a logical foundation for static bug-catching in quantum programming. The validity of formulas in this logic is dual to that of quantum Hoare logics. We justify the formulation of validity by an intuitive explanation from a reachability point of view and a comparison against several alternative formulations. Compared with existing works focusing on dynamic analysis, our logic provides sound and complete arguments. We further demonstrate the usefulness of the logic by reasoning several examples, including Grover’s search, quantum teleportation, and a repeat-until-success program. We also automate the reasoning procedure by a prototyped static analyzer built on top of the logic rules.
Sat 10 DecDisplayed time zone: Auckland, Wellington change
13:30 - 15:00 | |||
13:30 30mResearch paper | On incorrectness logic for Quantum programs OOPSLA Peng Yan University of Technology Sydney, Hanru Jiang Yanqi Lake Beijing Institute of Mathematical Sciences and Applications, China, Nengkun Yu Stony Brook University, USA DOI | ||
14:00 30mResearch paper | Weighted programming: a programming paradigm for specifying mathematical models OOPSLA Kevin Batz RWTH Aachen University, Adrian Gallus RWTH Aachen University, Benjamin Lucien Kaminski Saarland University and University College London, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University DOI | ||
14:30 30mTalk | Wildcards Need Witness Protection OOPSLA Kevin Bierhoff Google DOI |