SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Sat 10 Dec 2022 13:30 - 14:00 at Seminar Room G007 - Logic and Verification II Chair(s): Atsushi Igarashi

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 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
Logic and Verification IIOOPSLA at Seminar Room G007
Chair(s): Atsushi Igarashi Kyoto University
13:30
30m
Research 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
30m
Research 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
30m
Talk
Wildcards Need Witness ProtectionDistinguished Paper
OOPSLA
DOI