A Unified Assertion-Based Framework for Classical-Quantum Program Verification
summary
Proposes an assertion-based verification framework that marks classical registers by classicality by subtype so all variables remain quantum but some satisfy measurability constraints, proves this isomorphic to the mapping-state approach, and replaces brittle predicates with modular lattice predicates (subspace terms plus expectation arithmetic). Uses multi-level assertions that compare expectation expressions and subspace terms, targets implementation inside an interactive theorem prover with automation, and aims to validate on real examples (Shor) and a compiler-to-circuit pipeline.
AI-written summary · about
chapters (12)
- 0:00Unified assertion framework intro
- 1:03Tool failures motivation
- 3:11Design goals for tools
- 5:44Classicality via subtyping
- 7:37Quantum predicate challenges
- 9:23Intuitive quantum predicates
- 11:51Interactive provers for quantum
- 13:59Multi-level assertions
- 16:34Verification framework blueprint
- 17:39Key takeaways and future
- 18:02Q&A: Comparison with Q
- 20:26Q&A: Disjunction in logic
related talks
27mAn Expressive Assertion Language for Quantum Programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
27mParameterized Verification of Quantum Circuits
16mProjection-Based Runtime Assertions for Testing and Debugging Quantum Programs
21mAnalyzing quantum programs using the power of interaction
42mQuantum program analysis: Verification and Testing
32mBeating Classical Impossibility of Position Verification
22mEfficient Formal Verification of Quantum Error Correcting Programs