QbC: Quantum Correctness by Construction
summary
Presents a method that builds quantum programs from pre/postconditions by applying sound and complete refinement rules over a quantum while language, using quantum Hoare logic with POVM predicates and denotational CP maps. Demonstrates patterns like repeat‑until‑success with an explicit epsilon success probability and a termination condition, shows how bounded and unbounded loop refinements produce families of intermediate assertions, and notes the work is currently theoretical with no implementation yet.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:05Horror logic and quantum extensions
- 2:28Correct by construction refinement
- 3:51Quantum While with holes
- 4:52Refinement rules for programs
- 6:18Loop refinements
- 8:05Repeat until success example
- 9:29Future directions
- 10:33Summary
- 10:54Q&A on oblivious amplitude amplification
- 11:15Comparison with synthesis
- 11:59Scalability and plans
- 12:20Weakest precondition calculus
related talks
22mQbC: Quantum Correctness by Construction
42mQuantum program analysis: Verification and Testing
30mOn incorrectness logic for Quantum programs
22mCoqQ: Foundational Verification of Quantum Programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
27mAn Expressive Assertion Language for Quantum Programs
22mEfficient Formal Verification of Quantum Error Correcting Programs