pith. sign in

arxiv: 2411.09121 · v2 · submitted 2024-11-14 · 💻 cs.LO · cs.FL

AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)

Yu-Fang Chen , Kai-Min Chung , Min-Hsiu Hsieh , Wei-Jia Huang , Ond\v{r}ej Leng\'al , Jyun-Ao Lin , Wei-Lun Tsai This is my paper

Pith reviewed 2026-05-23 17:58 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords quantum verificationquantum programsrepeat-until-successGrover searchloop invariantsmeasurementformal verification
0
0 comments X

The pith

AutoQ 2.0 verifies quantum programs with measurements and classical loops.

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

AutoQ 2.0 extends verification from quantum circuits to quantum programs that incorporate classical control flow. This requires new handling of measurements, normalization of quantum states, and techniques for verifying loops. The paper shows that the tool verifies all repeat-until-success algorithms instantly and the weak-measurement Grover search up to 100 qubits in roughly 20 minutes. A reader would care if they want to check the correctness of sophisticated quantum algorithms that depend on runtime decisions and feedback.

Core claim

AutoQ 2.0 is presented as a verifier that can handle quantum programs beyond circuits by addressing the treatment of measurement, the normalization problem, and lifting classical loop verification techniques. It has been used to verify the repeat-until-success algorithm and the weak-measurement-based version of Grover's search algorithm, with all benchmarks verified efficiently.

What carries the argument

Support for loop invariants in the input format together with the theoretical extensions for measurement and normalization.

If this is right

  • RUS algorithms are verified instantly.
  • Weak-measurement-based Grover search is verified for 100 qubits in about 20 minutes.
  • All benchmarks can be verified efficiently.

Where Pith is reading between the lines

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

  • This verification capability may support the development of more complex adaptive quantum algorithms.
  • Similar techniques could be used to verify other quantum programs that combine quantum operations with classical control.
  • Further engineering could allow verification of programs on even more qubits.

Load-bearing premise

The theoretical extensions for treatment of measurement, the normalization problem, and lifting of classical loop verification techniques to the quantum setting are implemented correctly and do not introduce undetected errors.

What would settle it

An experiment or manual check that reveals an error in a program that AutoQ 2.0 verified as correct, or a failure to verify a correct program among the benchmarks.

Figures

Figures reproduced from arXiv: 2411.09121 by Jyun-Ao Lin, Kai-Min Chung, Min-Hsiu Hsieh, Ond\v{r}ej Leng\'al, Wei-Jia Huang, Wei-Lun Tsai, Yu-Fang Chen.

Figure 1
Figure 1. Figure 1: The effect of applying selected quantum gates to state [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Intermediate states during the execution of Algorithm 1. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The LSTA recognizing the postcondition of Algorithm 1. In AutoQ 2.0, preconditions, postconditions, and invariants are represented as sets of quantum states, encoded using the LSTA model. Therefore, it is important for users to understand how to en￾code a set of quantum states with an LSTA. Below, we provide two examples to give a basic under￾standing of the process. In the first example, we show how to en… view at source ↗
Figure 4
Figure 4. Figure 4: The LSTA for Bell states and its textual description [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The architecture of AutoQ 2.0 4 System Architecture We present the architecture of AutoQ 2.0 in [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Computing 𝑓 ′ 𝑗 from 𝑓𝑖 . Formally, the algorithm performs a search in the directed graph (𝑉, 𝐸) (which is constructed on the fly), where vertices 𝑉 are of the form 𝑉 = (𝐷, {( 𝑓1, 𝑔1), . . . , ( 𝑓𝑚, 𝑔𝑚)}) where 𝐷 ⊆ 𝑄A is called the domain, each 𝑓𝑖 : 𝐷 → 2 𝑄B is a map that as￾signs every state of A from the do￾main 𝐷 a set of states of B, and each 𝑔𝑖 : term(C, X) → 2 term(C,X) is a (partial) mapping from te… view at source ↗
Figure 7
Figure 7. Figure 7: Intermediate states of Algorithm 6 7.1 The Weakly Measured Version of Grover’s Algorithm Algorithm 6: A Weakly Measured Version of Grover’s algorithm (solution 𝑠 = 0 𝑛 ) 1 Pre: {1 [PITH_FULL_IMAGE:figures/full_fig_p015_7.png] view at source ↗
read the original abstract

We present a verifier of quantum programs called AutoQ 2.0. Quantum programs extend quantum circuits (the domain of AutoQ 1.0) by classical control flow constructs, which enable users to describe advanced quantum algorithms in a formal and precise manner. The extension is highly non-trivial, as we needed to tackle both theoretical challenges (such as the treatment of measurement, the normalization problem, and lifting techniques for verification of classical programs with loops to the quantum world), and engineering issues (such as extending the input format with a~support for specifying loop invariants). We have successfully used AutoQ 2.0 to verify two types of advanced quantum programs that cannot be expressed using only quantum circuits: the \emph{repeat-until-success} (RUS) algorithm and the weak-measurement-based version of Grover's search algorithm. AutoQ 2.0 can efficiently verify all our benchmarks: all RUS algorithms were verified instantly and, for the weak-measurement-based version of Grover's search, we were able to handle the case of 100 qubits in $\sim$20 minutes.

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.

Referee Report

2 major / 1 minor

Summary. The paper presents AutoQ 2.0, an automated verifier extending AutoQ 1.0 from quantum circuits to quantum programs that incorporate classical control-flow constructs such as loops. It addresses theoretical challenges including the treatment of measurement, the normalization problem after measurement, and the lifting of classical loop-invariant techniques to the quantum setting, along with engineering extensions to the input format for specifying invariants. The central empirical claim is that these extensions enable sound and efficient verification of two classes of programs not expressible as circuits alone: repeat-until-success (RUS) algorithms (verified instantly) and a weak-measurement-based variant of Grover's search (handled for 100 qubits in approximately 20 minutes).

Significance. If the soundness of the measurement handling, normalization, and loop-lifting extensions holds, the work would constitute a meaningful step toward practical verification of quantum programs with classical control, moving beyond circuit-only tools. The reported scalability to 100 qubits on the Grover instance is a concrete strength that would be noteworthy if independently reproducible; however, the abstract supplies only runtime claims without derivation details, error bounds, or machine-checked soundness arguments for the extensions.

major comments (2)
  1. [Abstract and §1] Abstract and §1: the central claim that the listed theoretical extensions (measurement treatment, normalization, and lifting of classical loop techniques) have been resolved correctly rests on the weakest assumption identified in the reader's report; the manuscript provides no derivation details, soundness proof sketch, or independent check (e.g., comparison against a reference implementation or manual proof for a small instance) that would allow a reader to assess whether undetected errors were introduced.
  2. [Abstract] The efficiency claims for the 100-qubit Grover instance and the RUS benchmarks are presented without accompanying resource bounds, memory usage figures, or comparison against a baseline verifier that lacks the new extensions; this makes it impossible to isolate the contribution of the new components from implementation optimizations.
minor comments (1)
  1. [Abstract] The abstract mentions extending the input format to support loop invariants but does not indicate the concrete syntax or how invariants are checked for validity.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on the presentation of soundness arguments and experimental details. We address each major comment below and will revise the manuscript accordingly to improve clarity and verifiability of the claims.

read point-by-point responses

  1. Referee: [Abstract and §1] Abstract and §1: the central claim that the listed theoretical extensions (measurement treatment, normalization, and lifting of classical loop techniques) have been resolved correctly rests on the weakest assumption identified in the reader's report; the manuscript provides no derivation details, soundness proof sketch, or independent check (e.g., comparison against a reference implementation or manual proof for a small instance) that would allow a reader to assess whether undetected errors were introduced.

    Authors: We agree that a concise soundness sketch for the measurement handling, normalization after measurement, and lifting of loop invariants would strengthen the paper and allow readers to better assess the extensions. The full technical report contains the formal semantics and algorithm, but the abstract and §1 remain high-level. We will add a brief proof outline (e.g., in §3 or an appendix) in the revised version. revision: yes

  2. Referee: [Abstract] The efficiency claims for the 100-qubit Grover instance and the RUS benchmarks are presented without accompanying resource bounds, memory usage figures, or comparison against a baseline verifier that lacks the new extensions; this makes it impossible to isolate the contribution of the new components from implementation optimizations.

    Authors: The reported runtimes demonstrate practical verification of programs with classical control flow that prior circuit-only tools cannot handle. We will add peak memory usage figures from the experiments in the revision. A direct baseline comparison is difficult because no existing verifier supports the combination of measurements and loops in the same framework; AutoQ 1.0 is restricted to circuits. We will clarify this distinction in the text. revision: partial

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper presents an implementation of AutoQ 2.0 extending a prior circuit verifier to handle quantum programs with loops and measurements. Claims rest on successful verification runs for RUS and weak-measurement Grover instances (up to 100 qubits), with reported timings. No equations, fitted parameters, or load-bearing self-citations appear in the abstract or described content; the central results are empirical outcomes of the implemented extensions rather than derivations that reduce by construction to inputs or prior self-work. The work is self-contained as an engineering and tool paper whose soundness assumptions are isolated to the implementation correctness, not to any circular definitional step.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no explicit free parameters, axioms, or invented entities; the listed challenges (measurement treatment, normalization, lifting techniques) are treated as engineering tasks rather than new postulates.

pith-pipeline@v0.9.0 · 5757 in / 1117 out tokens · 47969 ms · 2026-05-23T17:58:26.300532+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

52 extracted references · 52 canonical work pages · 1 internal anchor

  1. [1]

    AutoQ 2.0 : An automata-based C++ tool for quantum program verification (Jan 2024), https://github.com/alan23273850/AutoQ/tree/CAV24

    work page 2024

  2. [2]

    under submission (2024)

    Abdulla, P.A., Chen, Y.G., Chen, Y.F., Hol´ık, L., Lengal, O., Lo, F.Y., Lin, J.A., Tsai, W.L.: Verifying quantum circuits with level-synchronized tree automata. under submission (2024)

    work page 2024

  3. [3]

    In: Esparza, J., Majumdar, R

    Abdulla, P.A., Chen, Y., Hol ´ık, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March...

    work page doi:10.1007/978-3-642-12002-2_14 2010

  4. [4]

    A Simple Proof that Toffoli and Hadamard are Quantum Universal

    Aharonov, D.: A simple proof that Toffoli and Hadamard are quantum universal (2003). https://doi.org/10.48550/arxiv.quant-ph/0301040, https://arxiv.org/abs/ quant-ph/0301040

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.quant-ph/0301040 2003

  5. [5]

    (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol

    Ahrendt, W., Beckert, B., Bubel, R., H¨ahnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol. 10001. Springer (2016).https://doi.org/10.1007/978-3-319-49812-6 , https://doi.org/10.1007/978-3-319-49812-6

    work page doi:10.1007/978-3-319-49812-6 2016

  6. [6]

    In: Quan- tum Physics and Logic (2018)

    Amy, M.: Towards large-scale functional verification of universal quantum circuits. In: Quan- tum Physics and Logic (2018)

    work page 2018

  7. [7]

    Quantum Science and Technology 7(2), 025007 (feb 2022)

    Andr ´es-Mart´ınez, P., Heunen, C.: Weakly measured while loops: peeking at quantum states. Quantum Science and Technology 7(2), 025007 (feb 2022). https://doi.org/10.1088/ 2058-9565/ac47f1, https://dx.doi.org/10.1088/2058-9565/ac47f1

    work page doi:10.1088/2058-9565/ac47f1 2022

  8. [8]

    In: Devitt, S.J., Lanese, I

    Anticoli, L., Piazza, C., Taglialegne, L., Zuliani, P.: Towards quantum programs verifica- tion: From Quipper circuits to QPMC. In: Devitt, S.J., Lanese, I. (eds.) Reversible Com- putation - 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Pro- ceedings. Lecture Notes in Computer Science, vol. 9720, pp. 213–219. Springer (2016). http...

    work page doi:10.1007/978-3-319-40578-0_16 2016

  9. [9]

    Baudin, P., Bobot, F., B¨ uhler, D., Correnson, L., Kirchner, F., Kosmatov, N., Maroneze, A., Perrelle, V., Prevosto, V., Signoles, J., Williams, N.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56–68 (2021). https://doi.org/10.1145/3470569

    work page doi:10.1145/3470569 2021

  10. [10]

    Springer Science & Business Media (2013)

    Bertot, Y., Cast ´eran, P.: Interactive theorem proving and program development: Coq’ Art: the calculus of inductive constructions. Springer Science & Business Media (2013)

    work page 2013

  11. [11]

    Bocharov, A., Roetteler, M., Svore, K.M.: Efficient synthesis of universal repeat- until-success quantum circuits. Phys. Rev. Lett. 114, 080502 (Feb 2015). https: //doi.org/10.1103/PhysRevLett.114.080502, https://link.aps.org/doi/10. 1103/PhysRevLett.114.080502

    work page doi:10.1103/physrevlett.114.080502 2015

  12. [12]

    In: Ibarra, O.H., Ravikumar, B

    Bouajjani, A., Habermehl, P., Hol ´ık, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Ibarra, O.H., Ravikumar, B. (eds.) Implementation and Applications of Automata, 13th International Conference, CIAA 2008, San Francisco, California, USA, July 21-24, 2008. Proceedings. Lectur...

    work page doi:10.1007/978-3-540-70844-5_7 2008

  13. [13]

    Boykin, P.O., Mor, T., Pulver, M., Roychowdhury, V.P., Vatan, F.: A new uni- versal and fault-tolerant quantum basis. Inf. Process. Lett. 75(3), 101–107 (2000). https://doi.org/10.1016/S0020-0190(00)00084-3, https://doi.org/10.1016/ S0020-0190(00)00084-3 17

    work page doi:10.1016/s0020-0190(00)00084-3 2000

  14. [14]

    IEEE Trans- actions on Computer-Aided Design of Integrated Circuits and Systems 40(9), 1810–1824 (2020)

    Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Trans- actions on Computer-Aided Design of Integrated Circuits and Systems 40(9), 1810–1824 (2020)

    work page 2020

  15. [15]

    Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verifi- cation framework for circuit-building quantum programs. In: Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Held as Part of the Euro- pean Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Lu...

    work page 2021

  16. [16]

    In: Yoshida, N

    Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verifica- tion framework for circuit-building quantum programs. In: Yoshida, N. (ed.) ESOP. Lecture Notes in Computer Science, vol. 12648, pp. 148–177. Springer International Publishing, Cham (March 2021)

    work page 2021

  17. [17]

    In: Proc

    Chen, T., Chen, Y., Jiang, J.R., Leng ´al, O., Jobranov ´a, S.: Accelerating quantum circuit simulation with symbolic execution and loop summarization. In: Proc. of ICCAD’24. ACM (2024)

    work page 2024

  18. [18]

    Quisp: a quantum internet simulation package,

    Chen, T.F., Jiang, J.H.R., Hsieh, M.H.: Partial equivalence checking of quantum circuits. In: 2022 IEEE International Conference on Quantum Computing and Engineering (QCE). pp. 594–604 (2022). https://doi.org/10.1109/QCE53715.2022.00082

    work page doi:10.1109/qce53715.2022.00082 2022

  19. [19]

    In: International Conference on Computer Aided Verification

    Chen, Y.F., Chung, K.M., Leng ´al, O., Lin, J.A., Tsai, W.L.: AutoQ: An automata-based quantum circuit verifier. In: International Conference on Computer Aided Verification. pp. 139–153. Springer (2023)

    work page 2023

  20. [20]

    In: 44th ACM SIGPLAN Conference on Programming Language Design and Implementation—PLDI’23

    Chen, Y., Chung, K., Leng ´al, O., Lin, J., Tsai, W., Yen, D.: An automata-based framework for verification and bug hunting in quantum circuits. In: 44th ACM SIGPLAN Conference on Programming Language Design and Implementation—PLDI’23. ACM (2023)

    work page 2023

  21. [21]

    New Journal of Physics 13(4), 043016 (apr 2011)

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

    work page 2011

  22. [22]

    In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M

    Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lec...

    work page doi:10.1007/978-3-642-03359-9_2 2009

  23. [23]

    De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14. pp. 337–340. Springer (2008)

    work page 2008

  24. [24]

    Mathematical Structures in Computer Science 16(3), 429–451 (2006)

    D’Hondt, E., Panangaden, P.: Quantum weakest preconditions. Mathematical Structures in Computer Science 16(3), 429–451 (2006)

    work page 2006

  25. [25]

    ACM Trans

    Fang, W., Ying, M., Wu, X.: Differentiable quantum programming with unbounded loops. ACM Trans. Softw. Eng. Methodol. 33(1) (nov 2023). https://doi.org/10.1145/ 3617178, https://doi.org/10.1145/3617178

    work page doi:10.1145/3617178 2023

  26. [26]

    ACM Transactions on Quantum Computing 2(4), 1–43 (2021)

    Feng, Y., Ying, M.: Quantum Hoare logic with classical variables. ACM Transactions on Quantum Computing 2(4), 1–43 (2021)

    work page 2021

  27. [27]

    Feng, Y., Yu, N., Ying, M.: Model checking quantum Markov chains. J. Comput. Syst. Sci. 79(7), 1181–1198 (2013). https://doi.org/10.1016/j.jcss.2013.04.002, https: //doi.org/10.1016/j.jcss.2013.04.002

    work page doi:10.1016/j.jcss.2013.04.002 2013

  28. [28]

    Filli ˆatre, J.C., Paskevich, A.: Why3—where programs meet provers. In: Programming Lan- guages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part 18 of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 22. pp. 125–128. Springer (2013)

    work page 2013

  29. [29]

    In: Mathematical Aspects of Computer Science

    Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science. pp. 19–32. Proceedings of Symposia in Applied Mathematics, AMS (1967), https://mathscinet.ams.org/mathscinet/article?mr=235771

    work page 1967

  30. [30]

    Preskill

    Grover, L.K.: A fast quantum mechanical algorithm for database search. 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, https://doi.org/10.1145/237814.237866

    work page doi:10.1145/237814.237866 1996

  31. [31]

    In: Steffen, B., Woeginger, G.J

    H ¨ahnle, R., Huisman, M.: Deductive software verification: From pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G.J. (eds.) Computing and Software Science - State of the Art and Perspectives, Lecture Notes in Computer Science, vol. 10000, pp. 345–

    work page

  32. [32]

    https://doi.org/10.1007/978-3-319-91908-9_18 , https:// doi.org/10.1007/978-3-319-91908-9_18

    Springer (2019). https://doi.org/10.1007/978-3-319-91908-9_18 , https:// doi.org/10.1007/978-3-319-91908-9_18

    work page doi:10.1007/978-3-319-91908-9_18 2019

  33. [33]

    arXiv preprint arXiv:1904.06319 (2019)

    Hietala, K., Rand, R., Hung, S.H., Wu, X., Hicks, M.: Verified optimization in a quantum intermediate representation. arXiv preprint arXiv:1904.06319 (2019)

    work page arXiv 1904

  34. [34]

    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259, https://doi.org/10. 1145/363235.363259

    work page doi:10.1145/363235.363259 1969

  35. [35]

    In: Bultan, T., Hsiung, P

    Hol ´ık, L., Leng´al, O., Sim ´acek, J., Vojnar, T.: Efficient inclusion checking on explicit and semi-symbolic tree automata. In: Bultan, T., Hsiung, P. (eds.) Automated Technology for Verification and Analysis, 9th International Symposium, ATV A 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6996, pp. 243...

    work page doi:10.1007/978-3-642-24372-1_18 2011

  36. [36]

    In: Ueda, K

    Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Ueda, K. (ed.) Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Shanghai, China, November 28 - December 1, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6461, pp. 304–311. Springer (2010).https://doi.org/10.1007/ 978-3-642-17164-2_21 , ...

    work page doi:10.1007/978-3-642-17164-2_21 2010

  37. [37]

    In: Clarke, E.M., Voronkov, A

    Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol. 6355, pp. 348–370. Springer (201...

    work page doi:10.1007/978-3-642-17511-4_20 2010

  38. [38]

    In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems

    Leng ´al, O., ˇSim´aˇcek, J., Vojnar, T.: V ATA: A library for efficient manipulation of non- deterministic tree automata. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 79–94. Springer (2012)

    work page 2012

  39. [39]

    In: International conference on computer aided verification

    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: International conference on computer aided verification. pp. 187–207. Springer (2019)

    work page 2019

  40. [40]

    Mateus, P., Ramos, J., Sernadas, A., Sernadas, C.: Temporal Logics for Reasoning about Quantum Systems, p. 389–413. Cambridge University Press (2009). https://doi.org/ 10.1017/CBO9781139193313.011

    work page doi:10.1017/cbo9781139193313.011 2009

  41. [41]

    Quantum Info

    Paetznick, A., Svore, K.M.: Repeat-until-success: Non-deterministic decomposition of single- qubit unitaries. Quantum Info. Comput. 14(15–16), 1277–1301 (nov 2014)

    work page 2014

  42. [42]

    In: International Static Analysis Symposium

    Perdrix, S.: Quantum entanglement analysis based on abstract interpretation. In: International Static Analysis Symposium. pp. 270–282. Springer (2008)

    work page 2008

  43. [43]

    In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

    Unruh, D.: Quantum Hoare logic with ghost variables. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–13. IEEE (2019) 19

    work page 2019

  44. [44]

    In: Proceedings of the 59th ACM/IEEE Design Automation Conference

    Wei, C.Y., Tsai, Y.H., Jhang, C.S., Jiang, J.H.R.: Accurate bdd-based unitary operator ma- nipulation for scalable and robust quantum circuit verification. In: Proceedings of the 59th ACM/IEEE Design Automation Conference. p. 523–528. DAC ’22, Association for Com- puting Machinery, New York, NY, USA (2022). https://doi.org/10.1145/3489517. 3530481, https:...

    work page doi:10.1145/3489517 2022

  45. [45]

    In: Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008

    Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings 21. pp. 33–38. Springer (2008)

    work page 2008

  46. [46]

    Xu, M., Fu, J., Mei, J., Deng, Y.: Model checking QCTL plus on quantum Markov chains. Theor. Comput. Sci. 913, 43–72 (2022). https://doi.org/10.1016/j.tcs.2022.01. 044, https://doi.org/10.1016/j.tcs.2022.01.044

    work page doi:10.1016/j.tcs.2022.01 2022

  47. [47]

    In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

    Xu, M., Li, Z., Padon, O., Lin, S., Pointing, J., Hirth, A., Ma, H., Palsberg, J., Aiken, A., Acar, U.A., et al.: Quartz: superoptimization of quantum circuits. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 625–640 (2022)

    work page 2022

  48. [48]

    ACM Transactions on Programming Languages and Systems (TOPLAS) 33(6), 1–49 (2012)

    Ying, M.: Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 33(6), 1–49 (2012)

    work page 2012

  49. [49]

    In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

    Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 542–558 (2021)

    work page 2021

  50. [50]

    Proceedings of the ACM on Programming Languages 7(POPL), 833–865 (2023)

    Zhou, L., Barthe, G., Strub, P.Y., Liu, J., Ying, M.: Coqq: Foundational verification of quantum programs. Proceedings of the ACM on Programming Languages 7(POPL), 833–865 (2023)

    work page 2023

  51. [51]

    In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

    Zhou, L., Yu, N., Ying, M.: An applied quantum Hoare logic. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 1149–1162 (2019)

    work page 2019

  52. [52]

    In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

    Zhu, S., Hung, S.H., Chakrabarti, S., Wu, X.: On the principles of differentiable quan- tum programming languages. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 272–285. PLDI 2020, Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/ 3385412.3386011, https://doi....

    work page doi:10.1145/3385412.3386011 2020