SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…)
summary
SAQR-QC combines quantum Hoare-style inequalities with quantum abstract interpretation to trade exactness for speed: each reasoning step touches only local reduced density matrices (small qubit sets) so no 2^n matrices are built, and accumulated error is tracked so precision remains bounded. It handles one- and two-qubit unitaries, verifies GHZ circuits with non‑Clifford gates recovering the 1/√2 amplitude (misses a global phase), and analyzes quantum phase estimation, demonstrating scalable but approximate verification.
AI-written summary · about
chapters (10)
- 0:00Quantum programming models
- 1:52Quantum Hoare logic limits
- 5:39Scalability in quantum reasoning
- 8:05Quantum abstract interpretation + Hoare logic
- 11:14Quantitative reasoning with observers
- 13:41Scalable verification workflow
- 14:46Demo: CNOT and GHZ circuits
- 15:27Future work and questions
- 15:48Q&A: Symbolic operators
- 16:50Q&A: BQP verification
related talks
42mQuantum program analysis: Verification and Testing
22mQbC: Quantum Correctness by Construction
52mThe Virtues of the Quantum Approximate Optimization Algorithm
13mQbC: Quantum Correctness by Construction
22mEfficient Formal Verification of Quantum Error Correcting Programs
44mQuantum Meets Minimum Circuit Size Problem
18mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
35mQuantum relational Hoare logic, towards a formalization