arxiv: 2605.05786 · v1 · submitted 2026-05-07 · 💻 cs.LO · cs.FL

Recognition: unknown

A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)

Ond\v{r}ej Leng\'al, Wei-Lun Tsai, Yu-Fang Chen

Authors on Pith no claims yet

Pith reviewed 2026-05-08 04:55 UTC · model grok-4.3

classification 💻 cs.LO cs.FL

keywords quantum program verificationHoare logicspecification languageautomata-based verificationlinear complexityset-based assertionsquantum programs

0 comments

The pith

An extended set-based language with linear-complexity translation to automata enables automatic Hoare-style verification of larger fixed-qubit quantum programs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces an extended set-based specification language for quantum programs and an algorithm to translate these specifications into automata. The translation runs in time linear in the number of qubits by relying on controlled automaton construction and qubit reordering. The compact automata produced support fully automatic verification of programs with fixed qubit counts at scales that were previously out of reach while increasing the range of expressible properties.

Core claim

We introduce an extended set-based specification language and a specification-to-automata translation algorithm whose complexity is linear in the number of qubits, enabled by controlled automaton construction and qubit reordering. The resulting compact automata enable fully automatic Hoare-style verification of fixed-qubit quantum programs at previously infeasible scales, while substantially improving expressiveness without compromising efficiency.

What carries the argument

The specification-to-automata translation algorithm that achieves linear complexity in the number of qubits through controlled automaton construction and qubit reordering.

If this is right

Automatic verification becomes feasible for quantum programs using more qubits than before.
Specifications can express more properties while verification remains efficient.
Hoare-style reasoning about quantum programs can be performed without manual intervention at larger scales.
Compact automata reduce the practical barrier to checking correctness of fixed-qubit algorithms.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The linear translation removes the exponential blow-up that previously blocked automation in similar frameworks.
The same controlled-construction idea could be tested on other quantum reasoning tasks that currently suffer from state-space explosion.
If the reordering step generalizes, it might support limited forms of qubit allocation without losing the linear bound.

Load-bearing premise

Quantum programs use a fixed number of qubits and all relevant correctness properties can be written in the extended set-based language without causing exponential resource costs during verification.

What would settle it

A specification whose translation to automata requires more than linear time in the qubit count, or a fixed-qubit program whose resulting automata are too large for the verification procedure to finish automatically.

Figures

Figures reproduced from arXiv: 2605.05786 by Ond\v{r}ej Leng\'al, Wei-Lun Tsai, Yu-Fang Chen.

**Figure 1.** Figure 1: Representing a set of quantum states with an LSTA (𝑞1, 𝑞2), 𝑞0 {2} −−→ (𝑞2, 𝑞3), 𝑞1 {1} −−→ (𝑞4, 𝑞5), 𝑞2 {1} −−→ (𝑞6, 𝑞6), 𝑞3 {1} −−→ (𝑞7, 𝑞8)}, Δex = { 𝑞4 {1} −−→ 1 √ 2 , 𝑞5 {1} −−→ −1 √ 2 , 𝑞6 {1} −−→ 0, 𝑞7 {1} −−→ 𝑖 √ 2 , 𝑞8 {1} −−→ −𝑖 √ 2 }, 𝑟 = 𝑞0. In view at source ↗

**Figure 2.** Figure 2: Syntax of the specification language. The grammar comprises six terminal categories: natural number N ∈ N; constant binary string CStr ∈ {0, 1} + ; complex polynomial 𝛼 ∈ C[𝑉𝑐]; binary string variable V ∈ 𝑉𝑠; constraint CCons, defined as a quantifier-free first-order formula in nonlinear arithmetic over the real part and imaginary part of variables in 𝑉𝑐; and basis string pattern VStr ∈ ({0, 1} ∪𝑉𝑠 ∪𝑉𝑠) + … view at source ↗

**Figure 3.** Figure 3: 3-qubit BV circuit. An oracle circuit is a black-box circuit that encodes a function and enables quantum algorithms to query information in a single step. In Grover’s search [22], the oracle implements 𝑓 (𝑥): B 𝑛 → B, returning 1 on the marked solution 𝑥 and 0 otherwise; in Bernstein–Vazirani (BV) [6], it encodes a secret bit string. To verify such algorithms for all oracles, we use a parameterized oracl… view at source ↗

**Figure 4.** Figure 4: Multi-controlled Toffoli with 5 control qubits. Standard Toffoli gates have two • as controls and one ⊕ as the target. Quantum hardware typically supports only a limited gate set, so implementing an unsupported gate often requires decomposing it into a sequence of native gates. For example, an 𝑛-controlled Toffoli gate is usually realized using standard Toffoli gates. In view at source ↗

**Figure 5.** Figure 5: Dependency graph for slot indices based on 𝑆𝐴 and 𝑆𝐵. Solid blue lines indicate recurrence dependencies (shared variables), and dashed red lines indicate inequality constraints. The graph reveals three disjoint connected components. In each component, the numbers are arranged in ascending order. In the whole graph, the components are arranged in ascending order of their minimum elements. Tensor Product Tra… view at source ↗

read the original abstract

Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification. While automata-based verification scales well when specifications are given directly as automata, prior frameworks incur exponential blow-up when translating high-level set-based assertions into automata, which severely limits practicality. We introduce an extended set-based specification language and a specification-to-automata translation algorithm whose complexity is linear in the number of qubits, enabled by controlled automaton construction and qubit reordering. The resulting compact automata enable fully automatic Hoare-style verification of fixed-qubit quantum programs at previously infeasible scales, while substantially improving expressiveness without compromising efficiency.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper gives a linear-time translation from an extended set-based spec language to automata for quantum Hoare verification via controlled construction and qubit reordering.

read the letter

The key takeaway is that the authors have a way to turn high-level set-based assertions into automata without the exponential cost that blocked automatic verification before. They do this for fixed-qubit programs by extending the language and using controlled automaton construction plus qubit reordering to keep the translation linear in the number of qubits. The full paper supplies the definitions, the algorithm, and the complexity argument, which directly addresses the practicality barrier in quantum formal methods. That is the concrete advance here, and it improves expressiveness while preserving the efficiency needed for larger scales. The construction looks sound on the details provided, with no hidden exponential factors or circular steps apparent. The main soft spots are the fixed-qubit restriction, which is stated up front, and the requirement that properties fit inside their extended set language. If a spec needs something outside that or involves dynamic qubit allocation, the method does not apply. Post-translation checking costs are left as future work, but that is outside their central claim. This is for researchers building or using verification tools for quantum software. Anyone working on scaling Hoare logic or automata-based checks in this area will find the algorithm useful. It has enough technical substance and addresses a real limitation in prior approaches to deserve a serious referee. I would send it through peer review.

Referee Report

0 major / 2 minor

Summary. The paper introduces an extended set-based specification language for quantum programs together with a specification-to-automata translation algorithm whose complexity is linear in the number of qubits. The linearity is achieved via controlled automaton construction and qubit reordering; the resulting compact automata support fully automatic Hoare-style verification of fixed-qubit quantum programs at scales that were previously infeasible due to exponential blow-up in prior translation methods.

Significance. If the linearity and soundness claims hold, the work provides a practical route to automatic verification of quantum programs with more qubits than existing set-based approaches permit. The combination of improved expressiveness and linear scaling is a concrete advance for the field of quantum program verification.

minor comments (2)

Abstract: the phrase 'substantially improving expressiveness' is stated without a concrete example or comparison metric; a brief illustrative specification that could not be expressed in prior languages would strengthen the claim.
The manuscript should clarify in the complexity argument whether the controlled construction remains linear when the specification contains nested set operations whose size grows with the number of qubits.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our contribution, the assessment of its significance, and the recommendation for minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper presents a constructive algorithmic result: an extended set-based specification language together with an explicit specification-to-automata translation whose claimed linear complexity is justified by the definitions of controlled automaton construction and qubit reordering given inside the manuscript. These are new definitions and an algorithm supplied by the authors, not a derivation that reduces by construction to prior fitted parameters, self-referential equations, or load-bearing self-citations. The Hoare-style verification claim follows directly from the soundness of the translation and the compactness of the resulting automata, all argued within the paper itself without importing uniqueness theorems or ansatzes from overlapping prior work. The contribution is therefore self-contained as a practical specification method.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work extends established Hoare logic and automata constructions for quantum programs without introducing new free parameters or invented entities; it relies on standard formal methods background.

axioms (2)

standard math Hoare logic provides a sound foundation for reasoning about quantum program correctness
The entire verification approach is built on Hoare-style triples adapted to quantum semantics.
domain assumption Automata can faithfully represent the behavior of quantum programs under the chosen semantics
The translation targets automata-based verification, assuming this representation is adequate.

pith-pipeline@v0.9.0 · 5409 in / 1352 out tokens · 50643 ms · 2026-05-08T04:55:31.565696+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

45 extracted references · 34 canonical work pages · 1 internal anchor

[1]

Abdulla, P.A., Chen, Y., Chen, Y., Holík, L., Lengál, O., Lin, J., Lo, F., Tsai, W.: Veri- fying quantum circuits with level-synchronized tree automata. Proc. ACM Program. Lang. 9(POPL), 923–953 (2025).https://doi.org/10.1145/3704868

work page doi:10.1145/3704868 2025
[2]

Abdulla, P.A., Chen, Y.F., Hečko, M., Holík, L., Lengál, O., Lin, J.A., Thinniyam, R.S.: Parameterized verification of quantum circuits. Proc. ACM Program. Lang.10(POPL) (Jan 2026).https://doi.org/10.1145/3776712

work page doi:10.1145/3776712 2026
[3]

In: Selinger, P., Chiribella, G

Amy, M.: Towards large-scale functional verification of universal quantum circuits. In: Selinger, P., Chiribella, G. (eds.) Proceedings 15th International Conference on Quantum PhysicsandLogic,QPL2018,Halifax,Canada,3-7thJune2018.EPTCS,vol.287,pp.1–21 (2018).https://doi.org/10.4204/EPTCS.287.1

work page doi:10.4204/eptcs.287.1 2018
[4]

Nature574, 505–510 (2019).https://doi.org/10.1038/ s41586-019-1666-5

Arute, F., Arya, K., Babbush, R., et al.: Quantum supremacy using a programmable superconducting processor. Nature574, 505–510 (2019).https://doi.org/10.1038/ s41586-019-1666-5

2019
[5]

In: Chechik, M., Katoen, J., Leucker, M

Bauer-Marquart, F., Leue, S., Schilling, C.: symqv: Automated symbolic verification of quantum programs. In: Chechik, M., Katoen, J., Leucker, M. (eds.) Formal Methods - 25th Title Suppressed Due to Excessive Length 21 International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings. pp. 181–198. Lecture Notes in Computer Science, Springer...

2023
[6]

(eds.) Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA

Bernstein,E.,Vazirani,U.V.:Quantumcomplexitytheory.In:Kosaraju,S.R.,Johnson,D.S., Aggarwal, A. (eds.) Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA. pp. 11–20. ACM (1993).https: //doi.org/10.1145/167088.167097

work page doi:10.1145/167088.167097 1993
[7]

Birkhoff and J

Birkhoff, G., von Neumann, J.: The logic of quantum mechanics. Annals of Mathematics 37(4), 823–843 (1936).https://doi.org/10.2307/1968621

work page doi:10.2307/1968621 1936
[8]

In: ASPDAC ’21: 26th Asia and South Pacific Design Automa- tion Conference, Tokyo, Japan, January 18-21, 2021

Burgholzer, L., Kueng, R., Wille, R.: Random stimuli generation for the verification of quantum circuits. In: ASPDAC ’21: 26th Asia and South Pacific Design Automa- tion Conference, Tokyo, Japan, January 18-21, 2021. pp. 767–772. ACM (2021).https: //doi.org/10.1145/3394885.3431590

work page doi:10.1145/3394885.3431590 2021
[9]

Burgholzer,L.,Wille,R.:Advancedequivalencecheckingforquantumcircuits.IEEETrans. Comput. Aided Des. Integr. Circuits Syst.40(9), 1810–1824 (2021).https://doi.org/ 10.1109/TCAD.2020.3032630

work page doi:10.1109/tcad.2020.3032630 2021
[10]

In: Yoshida, N

Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: Yoshida, N. (ed.) Pro- gramming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Soft- ware, ETAPS 2021, ...

work page doi:10.1007/978-3-030-72019-3_6 2021
[11]

In: Xiong, J., Wille, R

Chen, T., Chen, Y., Jiang, J.R., Jobranová, S., Lengál, O.: Accelerating quantum circuit simulation with symbolic execution and loop summarization. In: Xiong, J., Wille, R. (eds.) Proceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design, ICCAD2024,NewarkLibertyInternationalAirportMarriott,NJ,USA,October27-31,2024. pp. 42:1–42:9. ...

work page doi:10.1145/3676536.3676711 2024
[12]

In: Gurfinkel, A., Heule, M

Chen, Y., Chung, K., Hsieh, M., Huang, W., Lengál, O., Lin, J., Tsai, W.: Autoq 2.0: From verification of quantum circuits to verification of quantum programs. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conference...

work page doi:10.1007/978-3-031-90660-2_5 2025
[13]

In: Enea, C., Lal, A

Chen, Y., Chung, K., Lengál, O., Lin, J., Tsai, W.: Autoq: An automata-based quantum circuit verifier. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference,CAV2023,Paris,France,July17-22,2023,Proceedings,PartIII.LectureNotes in Computer Science, vol. 13966, pp. 139–153. Springer (2023).https://doi.org/10. 1007/978-3-031...

2023
[14]

Chen, Y., Chung, K., Lengál, O., Lin, J., Tsai, W., Yen, D.: An automata-based framework for verification and bug hunting in quantum circuits. Proc. ACM Program. Lang.7(PLDI), 1218–1243 (2023).https://doi.org/10.1145/3591270

work page doi:10.1145/3591270 2023
[15]

Chen, Y., Chung, K., Lengál, O., Lin, J., Tsai, W., Yen, D.: An automata-based framework for verification and bug hunting in quantum circuits. Commun. ACM68(6), 85–93 (2025). https://doi.org/10.1145/3725728

work page doi:10.1145/3725728 2025
[16]

Lecture Notes in Computer Science, vol

Chen, Y., Rümmer, P., Tsai, W.: A theory of cartesian arrays (with applications in quantum circuitverification).In:Pientka,B.,Tinelli,C.(eds.)AutomatedDeduction-CADE29-29th InternationalConferenceonAutomatedDeduction,Rome,Italy,July1-4,2023,Proceedings. Lecture Notes in Computer Science, vol. 14132, pp. 170–189. Springer (2023).https: //doi.org/10.1007/97...

work page doi:10.1007/978-3-031-38499-8_10 2023
[17]

New Journal of Physics13(4), 043016 (2011).https://doi.org/10.1088/ 1367-2630/13/4/043016

Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and dia- grammatics. New Journal of Physics13(4), 043016 (2011).https://doi.org/10.1088/ 1367-2630/13/4/043016

2011
[18]

D’Hondt, E., Panangaden, P.: Quantum weakest preconditions. Math. Struct. Comput. Sci. 16(3), 429–451 (2006).https://doi.org/10.1017/S0960129506005251

work page doi:10.1017/s0960129506005251 2006
[19]

ACM Trans

Feng, Y., Ying, M.: Quantum hoare logic with classical variables. ACM Trans. Quantum Comput.2(4), 16:1–16:43 (2021).https://doi.org/10.1145/3456877

work page doi:10.1145/3456877 2021
[20]

ACM Trans

Feng,Y.,Zhou,L.,Xu,Y.,Xu,X.:Refinementcalculusofquantumprogramswithprojective assertions. ACM Trans. Softw. Eng. Methodol. (Oct 2025).https://doi.org/10.1145/ 3770083, just Accepted

2025
[21]

Greenberger, Michael A

Greenberger,D.M.,Horne,M.A.,Zeilinger,A.:GoingbeyondBell’stheorem.In:Kafatos,M. (ed.)Bell’sTheorem,QuantumTheoryandConceptionsoftheUniverse,pp.69–72.Springer Netherlands, Dordrecht (1989).https://doi.org/10.1007/978-94-017-0849-4_10

work page doi:10.1007/978-94-017-0849-4_10 1989
[22]

Grover,L.K.:Afastquantummechanicalalgorithmfordatabasesearch.In:Miller,G.L.(ed.) Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996. pp. 212–219. ACM (1996).https: //doi.org/10.1145/237814.237866

work page doi:10.1145/237814.237866 1996
[23]

Nature Physics17, 332–336 (2021).https://doi.org/10.1038/s41567-020-01105-y

Harrigan, M.P., Sung, K.J., Neeley, M., et al.: Quantum approximate optimization of non- planar graph problems on a planar superconducting processor. Nature Physics17, 332–336 (2021).https://doi.org/10.1038/s41567-020-01105-y

work page doi:10.1038/s41567-020-01105-y 2021
[24]

Evidence for the utility of quantum computing before fault tolerance

Kim, Y., et al.: Evidence for the utility of quantum computing before fault tolerance. Nature 618, 500–505 (2023).https://doi.org/10.1038/s41586-023-06096-3

work page doi:10.1038/s41586-023-06096-3 2023
[25]

(eds.) IEEE International Conference on Quantum Software, QSW 2024, Shenzhen, China, July 7-13, 2024

Lewis, M., Zuliani, P., Soudjani, S.: Automated verification of Silq quantum programs using SMTsolvers.In:Chang,R.N.,Chang,C.K.,Yang,J.,Jin,Z.,Sheng,M.,Fan,J.,Fletcher,K., He, Q., Faro, I., Leymann, F., Barzen, J., de la Puente, S., Feld, S., Wimmer, M., Atukorala, N., Wu, H., Elkouss, D., García-Alonso, J., Sarkar, A. (eds.) IEEE International Conference...

work page doi:10.1109/qsw62656.2024.00027 2024
[26]

and Churavy, Valentin and Paehler, Ludger and Hückelheim, Jan and Narayanan, Sri Hari Krishna and Schanen, Michel and Doerfert, Johannes , year =

Li,A.,Fang,B.,Granade,C.E.,Prawiroatmodjo,G.,Heim,B.,Roetteler,M.,Krishnamoorthy, S.: Sv-sim: scalable pgas-based state vector simulation of quantum circuits. In: de Supinski, B.R., Hall, M.W., Gamblin, T. (eds.) International Conference for High Performance Com- puting, Networking, Storage and Analysis, SC 2021, St. Louis, Missouri, USA, November 14-19, ...

work page doi:10.1145/3458817.3476169 2021
[27]

LIPIcs, vol.313,pp.24:1–24:31.SchlossDagstuhl-Leibniz-ZentrumfürInformatik(2024).https: //doi.org/10.4230/LIPICS.ECOOP.2024.24

Li,L.,Zhu,M.,Cleaveland,R.,Nicolellis,A.,Lee,Y.,Chang,L.,Wu,X.:Qafny:Aquantum- programverifier.In:Aldrich,J.,Salvaneschi,G.(eds.)38thEuropeanConferenceonObject- Oriented Programming, ECOOP 2024, Vienna, Austria, September 16-20, 2024. LIPIcs, vol.313,pp.24:1–24:31.SchlossDagstuhl-Leibniz-ZentrumfürInformatik(2024).https: //doi.org/10.4230/LIPICS.ECOOP.2024.24

work page doi:10.4230/lipics.ecoop.2024.24 2024
[28]

In: Dillig, I., Tasiran, S

Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Formal verification of quantum algorithms using quantum hoare logic. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. Lecture Notes in Computer Science, vol. 11...

work page doi:10.1007/978-3-030-25543-5_12 2019
[29]

Shor,P.W.:Algorithmsforquantumcomputation:Discretelogarithmsandfactoring.In:35th Annual Symposium on Foundations of Computer Science, Santa Fe, New Mexico, USA, November 20-22, 1994. pp. 124–134. IEEE Computer Society (1994).https://doi.org/ 10.1109/SFCS.1994.365700

work page doi:10.1109/sfcs.1994.365700 1994
[30]

In: Valiron, B., Mansfield, S., Arrighi, P., Panangaden, P

Singhal, K., Reppy, J.H.: Quantum hoare type theory: Extended abstract. In: Valiron, B., Mansfield, S., Arrighi, P., Panangaden, P. (eds.) Proceedings 17th International Conference onQuantumPhysicsandLogic,QPL2020,Paris,France,June2-6,2020.EPTCS,vol.340, pp. 291–302 (2020).https://doi.org/10.4204/EPTCS.340.15 Title Suppressed Due to Excessive Length 23

work page doi:10.4204/eptcs.340.15 2020
[31]

Stamatopoulos, N., Egger, D.J., Sun, Y., Zoufal, C., Iten, R., Shen, N., Woerner, S.: Option pricingusingquantumcomputers.Quantum4, 291(2020).https://doi.org/10.22331/ Q-2020-07-06-291

2020
[32]

Sundaram, A., Rand, R., Singhal, K., Lackey, B.: Hoare meets Heisenberg: A lightweight logic for quantum programs (2025),https://arxiv.org/abs/2101.08939

work page arXiv 2025
[33]

Zenodo.https://doi.org/10.5281/zenodo.19724316

Tsai, W.L., Chen, Y.F., Lengál, O.: A Practical Specification Language for Automatic Quan- tum Program Verification. Zenodo.https://doi.org/10.5281/zenodo.19724316

work page doi:10.5281/zenodo.19724316
[34]

In: 58th ACM/IEEE Design Automation Conference, DAC 2021, San Francisco,CA, USA,December5-9,2021

Tsai, Y., Jiang, J.R., Jhang, C.: Bit-slicing the hilbert space: Scaling up accurate quantum circuit simulation. In: 58th ACM/IEEE Design Automation Conference, DAC 2021, San Francisco,CA, USA,December5-9,2021. pp.439–444.IEEE(2021).https://doi.org/ 10.1109/DAC18074.2021.9586191

work page doi:10.1109/dac18074.2021.9586191 2021
[35]

In: 34th Annual ACM/IEEE Sympo- siumonLogicinComputerScience,LICS2019,Vancouver,BC,Canada,June24-27,2019

Unruh, D.: Quantum hoare logic with ghost variables. In: 34th Annual ACM/IEEE Sympo- siumonLogicinComputerScience,LICS2019,Vancouver,BC,Canada,June24-27,2019. pp. 1–13. IEEE (2019).https://doi.org/10.1109/LICS.2019.8785779

work page doi:10.1109/lics.2019.8785779 2019
[36]

Lang.6(OOPSLA1), 1–28 (2022).https://doi.org/10.1145/3527316

Yan,P.,Jiang,H.,Yu,N.:Onincorrectnesslogicforquantumprograms.Proc.ACMProgram. Lang.6(OOPSLA1), 1–28 (2022).https://doi.org/10.1145/3527316

work page doi:10.1145/3527316 2022
[37]

In: Gurfinkel,A.,Ganesh,V.(eds.)ComputerAidedVerification-36thInternationalConference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III

Yan, P., Jiang, H., Yu, N.: Approximate relational reasoning for quantum programs. In: Gurfinkel,A.,Ganesh,V.(eds.)ComputerAidedVerification-36thInternationalConference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. Lecture Notes in Computer Science, vol. 14683, pp. 495–519. Springer (2024).https://doi.org/10. 1007/978-3-031-65633-0_22

2024
[38]

Ying,M.:Floyd-Hoarelogicforquantumprograms.ACMTrans.Program.Lang.Syst.33(6), 19:1–19:49 (2011).https://doi.org/10.1145/2049706.2049708

work page doi:10.1145/2049706.2049708 2011
[39]

Younes,A.:StrengthandWeaknessinGrover’sQuantumSearchAlgorithm(2008),https: //arxiv.org/abs/0811.4481

work page arXiv 2008
[40]

Yu, N., Palsberg, J., Reps, T.: A logic for approximate quantitative reasoning about quantum circuits (2025),https://arxiv.org/abs/2507.13635

work page internal anchor Pith review Pith/arXiv arXiv 2025
[41]

Zhou,L.,Barthe,G.,Strub,P.,Liu,J.,Ying,M.:Coqq:Foundationalverificationofquantum programs. Proc. ACM Program. Lang.7(POPL), 833–865 (2023).https://doi.org/10. 1145/3571222

2023
[42]

In: McKinley, K.S., Fisher, K

Zhou, L., Yu, N., Ying, M.: An applied quantum hoare logic. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. pp. 1149–

2019
[43]

Proof.Given two LSTAsA=⟨𝑄 A, 𝑉A,Δ A, 𝑟A⟩andB=⟨𝑄 B, 𝑉B,Δ B, 𝑟B⟩, we compute their set unionA ⊔ Bas follows such thatL (A ⊔ B)=L (A) ∪ L (B)

ACM (2019).https://doi.org/10.1145/3314221.3314584 A Appendix A.1 Binary Operations of LSTA Lemma 11 (Semantics of LSTA Set Union).Given two LSTAsAandBoverK whereL (A)andL (B)contain𝑛-qubit and𝑚-qubit states, respectively, there exists a setunionoperation,denotedbyA ⊔B,whichyieldsavalidLSTAoverK.Therecognized language of the resulting LSTA satisfies: L (A...

work page doi:10.1145/3314221.3314584 2019
[44]

If𝛿 A 1 ≠𝛿 A 2 , then by the validity ofA, we have𝐶1 ∩𝐶 2 =∅
[45]

flip” (resp. “¬flip

If𝛿 A 1 =𝛿 A 2 , then we must have𝛿B 1 ≠𝛿 B 2 (otherwise𝛿 1 =𝛿 2). By the validity ofB, we have𝐷1 ∩𝐷 2 =∅. Ineithersubcase,theCartesianproduct(𝐶 1 ∩𝐶 2) × (𝐷 1 ∩𝐷 2)isempty,andhence ch(𝛿 1) ∩ch(𝛿 2)=∅. Sincedisjointnessholdsforallcases,A ⊗ Bsatisfiesthechoicedisjointnesscondition. ProofofL (A⊗B)=L (A)⊗L (B).Weprovetheequalitybyshowingmutualinclusion based...