On incorrectness logic for Quantum programs
summary
Proposes an incorrectness logic for quantum programs that treats predicates as projections and defines an under-approximation by projections relation to characterize erroneous states (duality with quantum Hoare triples). Gives formal denotational semantics for normal/error termination, derives proof rules (sequence, measurement, loop bounding) and proves the rule set sound and complete proof system for static bug-finding. Demonstrates on Grover, teleportation and repeat‑until‑success and ships a prototyped static analyzer automating the reasoning.
AI-written summary · about
chapters (20)
- 0:00Quantum program correctness
- 2:11Incorrectness logic in quantum
- 3:36Challenges in quantum logic
- 4:38Quantum predicates and projections
- 6:04Quantum semantics and control
- 7:07Quantum teleportation example
- 9:36Satisfaction in quantum logic
- 11:02Quantum reachability
- 12:28Classical versus quantum logic
- 13:11Quantum incorrectness triples
- 14:14Proof rules for quantum logic
- 15:37Bounded while rules
- 17:01Quantum simulation bug detection
- 17:44Summary of quantum logic
- 18:25Limitations and future work
- 19:40Q&A: Generalizing predicates
- 22:09Q&A: Loop invariants
- 23:57Q&A: Termination and variants
- 26:48Q&A: While rule triviality
- 27:48Q&A: Incorrectness specifications
related talks
42mQuantum program analysis: Verification and Testing
13mQbC: Quantum Correctness by Construction
22mQbC: Quantum Correctness by Construction
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
27mAn Expressive Assertion Language for Quantum Programs
22mEfficient Formal Verification of Quantum Error Correcting Programs
16mProjection-Based Runtime Assertions for Testing and Debugging Quantum Programs
14mDenotational semantics for stabiliser quantum programs