Quantum program analysis: Verification and Testing
summary
Survey of concrete program-analysis tools for quantum code: Quantum Hoare logic with sound and complete proof rules for partial and total correctness, a projection-based fragment that simplifies reasoning and preserves expressiveness via ancillas, and a Quantum Incorrectness logic for bug detection with approximations of reachable states. Presents a relational lifting and approximate quantum relational Hoare logic that gives explicit Delta bounds on output distance, and contrasts costly formal verification with statistically powered testing procedures.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:24Quantum verification and testing overview
- 5:02Classical to quantum Hoare logic
- 9:27Quantum operational semantics
- 17:32Projective quantum Hoare logic
- 25:01Quantum incorrect logic
- 25:24Quantum relational logic
- 30:13Approximate relational logic
- 30:33Testing versus verification
- 41:07Q&A
related talks
30mOn incorrectness logic for Quantum programs
13mQbC: Quantum Correctness by Construction
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
22mEfficient Formal Verification of Quantum Error Correcting Programs
22mCoqQ: Foundational Verification of Quantum Programs
22mQbC: Quantum Correctness by Construction
35mQuantum relational Hoare logic, towards a formalization
15mToward A Quantum Programming Language for Higher Level Formal Verification