The Landscape of Formal Verification in APL: a Review with a Case Study in Quantum(…)
summary
Claims that APL-style array language makes formal verification practical for quantum code by mapping a restricted QL/QPL subset to SMT checks and extracting invariants, pre/postconditions and safety/liveness properties. Implements a QV interpreter that translates QL primitives (H X Y Z, XX, parametric gates, state vectors) into queries for Z3 SMT and a static verifier; demonstrates simulation of small circuits (four-qubit Hadamard/random-number example) but currently verifies only simple gate families and not large-scale noisy hardware. Workflow-driven verification integrates simulator, translator and SMT backend.
AI-written summary · about
chapters (9)
- 0:00Formal verification in APL
- 1:51Quantum APL overview
- 3:43QV interpreter and verifier
- 5:52Formal Q program definition
- 8:19Correctness in quantum programs
- 11:11Verifying Deutsch-Jozsa algorithm
- 13:00Future of formal verification
- 14:05Summary
- 14:49Q&A
related talks
15mToward A Quantum Programming Language for Higher Level Formal Verification
22mEfficient Formal Verification of Quantum Error Correcting Programs
42mQuantum program analysis: Verification and Testing
40mDemocratizing quantum formal verification: the path-sum way
27mParameterized Verification of Quantum Circuits
33mVerified Compilation of Quantum Oracles
23mA Unified Assertion-Based Framework for Classical-Quantum Program Verification
41mQuantum Abstract Interpretation