Automating Quantum Hoare Logic with Automata (Work-In-Progress)
summary
Framework automates applied Quantum Hoare Logic by encoding projector assertions as sets of eigenvectors and eigenvalues using level-synchronized tree automata, claiming linear-size automata can represent exponential computational bases and supporting init, unitary, composition and loop rules when loop invariants are provided. It implements unitary/application by transforming automata, offers a custom inclusion-checker for Loewner/order checks, and constructs aQHL proof trees end-to-end for a repeat-until-success coin-flip example as proof of concept.
AI-written summary · about
chapters (11)
- 0:00Automating quantum Hoare logic
- 1:23Project challenges and goals
- 2:28Two-stage verification framework
- 3:34Generating skeleton proof trees
- 5:02Assertions with tree automata
- 6:31Level-synchronized tree automata example
- 10:10Proof rules with automata
- 13:25Initialization and linear operators
- 14:32Subspace inclusion checks
- 16:41Extending to full quantum Hoare logic
- 17:26Question and answer session
related talks
42mQuantum program analysis: Verification and Testing
35mQuantum relational Hoare logic, towards a formalization
15mToward A Quantum Programming Language for Higher Level Formal Verification
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
18mAn Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits
13mQbC: Quantum Correctness by Construction
27mParameterized Verification of Quantum Circuits
27mAn Expressive Assertion Language for Quantum Programs