QbC: Quantum Correctness by Construction
summary
Constructs quantum programs from pre/postconditions using typed holes and a set of refinement rules that reduce holes to initializations, unitaries, sequences and a while rule built from a convergent sequence of predicates; correctness is expressed with quantum predicates (measurements) and matrix inequalities in the Lowner order. The system is proved sound and complete. Examples: teleportation and Grover search are built stepwise — Grover yields Δ = 2α and R ≈ (π/4)√(N/T) to reach the target amplitude.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 0:44Program verification in quantum computing
- 3:11Correctness vs post-hoc verification
- 7:46Refinement rules and loops
- 9:35Soundness and completeness
- 11:23Grover’s algorithm step-by-step
- 16:41QbC framework advantages
- 17:28Q&A
related talks
13mQbC: Quantum Correctness by Construction
30mOn incorrectness logic for Quantum programs
42mQuantum program analysis: Verification and Testing
22mCoqQ: Foundational Verification of Quantum Programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
18mSAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…)
22mEfficient Formal Verification of Quantum Error Correcting Programs
01h 01mWhat Is "Quantum" About Quantum Computing?