A Static Analysis of Entanglement
summary
A static analysis based on abstract interpretation constructs an abstract domain that pairs a partition of qubits with per-block value labels (classical, X/uniform, S, top, bottom) and a special CNOT-separable relation to track when a CNOT can break entanglement. The analysis models programs as regex-like control flow with H T CNOT and measurements, is sound but intentionally over-approximating, loses precision after H on entangled blocks, and is not yet implemented for larger gate sets or a full language.
AI-written summary · about
chapters (8)
- 0:00Quantum entanglement analysis
- 5:58Quantum programming overview
- 8:49Entanglement tracking domain
- 12:02Representing qubit values
- 15:55Analysis of sample program
- 18:46Precision limits and improvements
- 20:10Q&A on gates and complexity
- 23:21Entanglement analysis matters
related talks
27mAbstracting Entanglement
20mTwist: Sound Reasoning for Purity and Entanglement in Quantum Programs
44mInvited talk: Twist: Sound Reasoning for Purity and Entanglement in Quantum P...
19mA Static Analysis for High-Level Quantum Programming Languages
41mQuantum Abstract Interpretation
20mA Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantu
42mQuantum program analysis: Verification and Testing
31mDemonstrating an Unconditional Separation Between Quantum and Classical Information Resources