On the public citation graph

Efficient Formal Verification of Quantum Error Correcting Programs

0 signed · 87 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.

Claim with ORCID

Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.

See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/978-3-030-17184-1_2openalex-snapshot

Meta-F $$^\star $$ : Proof Automation with SMT, Tactics, and Metaprograms

inferredcites →https://doi.org/10.1007/978-3-030-72019-3_6openalex-snapshot

An Automated Deductive Verification Framework for Circuit-building Quantum Programs

inferredcites →https://doi.org/10.1007/978-3-030-99524-9_24openalex-snapshot

cvc5: A Versatile and Industrial-Strength SMT Solver

inferredcites →https://doi.org/10.1007/978-3-031-27481-7_12openalex-snapshot

symQV: Automated Symbolic Verification of Quantum Programs

inferredcites →https://doi.org/10.1007/978-3-540-78800-3_24openalex-snapshot

Z3: An Efficient SMT Solver

inferredcites →https://doi.org/10.1007/978-3-642-10622-4_7openalex-snapshot

A Logic for Formal Verification of Quantum Programs

inferredcites →https://doi.org/10.1007/bf02283036openalex-snapshot

Effect algebras and unsharp quantum logics

inferredcites →https://doi.org/10.1007/s10817-020-09584-7openalex-snapshot

Certified Quantum Computation in Isabelle/HOL

inferredcites →https://doi.org/10.1016/b978-0-7506-8397-5.x0001-3openalex-snapshot

Digital Systems Design with FPGAs and CPLDs

inferredcites →https://doi.org/10.1016/c2022-0-02250-9openalex-snapshot

Foundations of Quantum Programming

inferredcites →https://doi.org/10.1016/j.entcs.2006.04.003openalex-snapshot

Reasoning About Imperative Quantum Programs

inferredcites →https://doi.org/10.1016/j.tcs.2007.06.011openalex-snapshot

Proof rules for the correctness of quantum programs

inferredcites →https://doi.org/10.1017/s0960129506005251openalex-snapshot

Quantum weakest preconditions

inferredcites →https://doi.org/10.1038/s41467-021-22274-1openalex-snapshot

The XZZX surface code

inferredcites →https://doi.org/10.1038/s41586-022-05434-1openalex-snapshot

Suppressing quantum errors by scaling a surface code logical qubit

inferredcites →https://doi.org/10.1038/s41586-023-06927-3openalex-snapshot

Logical quantum processor based on reconfigurable atom arrays

inferredcites →https://doi.org/10.1038/s41586-024-07107-7openalex-snapshot

High-threshold and low-overhead fault-tolerant quantum memory

inferredcites →https://doi.org/10.1038/s41586-024-08449-yopenalex-snapshot

Quantum error correction below the surface code threshold

inferredcites →https://doi.org/10.1063/1.1499754openalex-snapshot

Topological quantum memory

inferredcites →https://doi.org/10.1070/rm1997v052n06abeh002155openalex-snapshot

Quantum computations: algorithms and error correction

inferredcites →https://doi.org/10.1088/1367-2630/13/4/043016openalex-snapshot

Interacting quantum observables: categorical algebra and diagrammatics

inferredcites →https://doi.org/10.1088/1367-2630/17/8/083026openalex-snapshot

Unfolding the color code

inferredcites →https://doi.org/10.1098/rspa.1996.0136openalex-snapshot

Multiple-particle interference and quantum error correction

inferredcites →https://doi.org/10.1103/physreva.54.1098openalex-snapshot

Good quantum error-correcting codes exist

inferredcites →https://doi.org/10.1103/physreva.70.052328openalex-snapshot

Improved simulation of stabilizer circuits

inferredcites →https://doi.org/10.1103/physreva.73.022334openalex-snapshot

Fast simulation of stabilizer circuits using a graph-state representation

inferredcites →https://doi.org/10.1103/physreva.86.052329openalex-snapshot

Magic-state distillation with low overhead

inferredcites →https://doi.org/10.1103/physreva.95.022316openalex-snapshot

Unified framework for magic state distillation and multiqubit gate synthesis with reduced resource cost

inferredcites →https://doi.org/10.1103/physrevlett.129.030501openalex-snapshot

Realization of an Error-Correcting Surface Code with Superconducting Qubits

inferredcites →https://doi.org/10.1103/physrevx.11.041058openalex-snapshot

Realization of Real-Time Fault-Tolerant Quantum Error Correction

inferredcites →https://doi.org/10.1103/prxquantum.2.040101openalex-snapshot

Quantum Low-Density Parity-Check Codes

inferredcites →https://doi.org/10.1109/18.681315openalex-snapshot

Quantum error correction via codes over GF(4)

inferredcites →https://doi.org/10.1109/18.771249openalex-snapshot

Quantum Reed-Muller codes

inferredcites →https://doi.org/10.1109/focs54457.2022.00117openalex-snapshot

Quantum Tanner codes

inferredcites →https://doi.org/10.1109/isit.2012.6284206openalex-snapshot

Improved quantum hypergraph-product LDPC codes

inferredcites →https://doi.org/10.1109/isit.2013.6620283openalex-snapshot

Leveraging automorphisms of quantum codes for fault-tolerant quantum computation

inferredcites →https://doi.org/10.1109/lics.2019.8785779openalex-snapshot

Quantum Hoare Logic with Ghost Variables

inferredcites →https://doi.org/10.1109/lics52264.2021.9470673openalex-snapshot

A Quantum Interpretation of Bunched Logic & Quantum Separation Logic

inferredcites →https://doi.org/10.1109/tit.2013.2292061openalex-snapshot

Quantum LDPC Codes With Positive Rate and Minimum Distance Proportional to the Square Root of the Blocklength

inferredcites →https://doi.org/10.1126/science.1253742openalex-snapshot

Quantum computations on a topologically encoded qubit

inferredcites →https://doi.org/10.1142/s0219749904000067openalex-snapshot

DYNAMIC QUANTUM LOGIC FOR QUANTUM PROGRAMS

inferredcites →https://doi.org/10.1145/2049706.2049708openalex-snapshot

Floyd--hoare logic for quantum programs

inferredcites →https://doi.org/10.1145/2837614.2837655openalex-snapshot

Dependent types and multi-monadic effects in F*

inferredcites →https://doi.org/10.1145/3009837.3009894openalex-snapshot

QWIRE: a core language for quantum circuits

inferredcites →https://doi.org/10.1145/3290346openalex-snapshot

Quantum relational Hoare logic

inferredcites →https://doi.org/10.1145/3314221.3314584openalex-snapshot

An applied quantum Hoare logic

inferredcites →https://doi.org/10.1145/3371089openalex-snapshot

Relational proofs for quantum programs

inferredcites →https://doi.org/10.1145/3434318openalex-snapshot

A verified optimizer for Quantum circuits

inferredcites →https://doi.org/10.1145/3445814.3446750openalex-snapshot

Logical abstractions for noisy variational Quantum algorithm simulation

inferredcites →https://doi.org/10.1145/3453483.3454061openalex-snapshot

Quantum abstract interpretation

inferredcites →https://doi.org/10.1145/3456877openalex-snapshot

Quantum Hoare Logic with Classical Variables

inferredcites →https://doi.org/10.1145/3498697openalex-snapshot

A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic

inferredcites →https://doi.org/10.1145/3519939.3523431openalex-snapshot

Giallar: push-button verification for the qiskit Quantum compiler

inferredcites →https://doi.org/10.1145/3571222openalex-snapshot

CoqQ: Foundational Verification of Quantum Programs

inferredcites →https://doi.org/10.1145/3571786.3573018openalex-snapshot

Symbolic Execution of Hadamard-Toffoli Quantum Circuits

inferredcites →https://doi.org/10.1145/3591270openalex-snapshot

An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits

inferredcites →https://doi.org/10.1145/3624483openalex-snapshot

Formal Verification of Quantum Programs: Theory, Tools, and Challenges

inferredcites →https://doi.org/10.1145/3656419openalex-snapshot

Symbolic Execution for Quantum Error Correction Programs

inferredcites →https://doi.org/10.1145/3729293openalex-snapshot

Efficient Formal Verification of Quantum Error Correcting Programs

inferredcites →https://doi.org/10.22331/q-2018-08-06-79openalex-snapshot

Quantum Computing in the NISQ era and beyond

inferredcites →https://doi.org/10.22331/q-2021-07-06-497openalex-snapshot

Stim: a fast stabilizer circuit simulator

inferredcites →https://doi.org/10.4204/eptcs.266.8openalex-snapshot

QWIRE Practice: Formal Verification of Quantum Circuits in Coq

inferredcites →https://doi.org/10.4204/eptcs.287.1openalex-snapshot

Towards Large-scale Functional Verification of Universal Quantum Circuits

inferredcites →https://doi.org/10.4204/eptcs.287.17openalex-snapshot

ReQWIRE: Reasoning about Reversible Quantum Circuits

inferredcites →https://doi.org/10.4204/eptcs.318.14openalex-snapshot

PyZX: Large Scale Automated Diagrammatic Reasoning

inferredcites →https://doi.org/10.4204/eptcs.340.14openalex-snapshot

Gottesman Types for Quantum Programs

inferredcites →https://doi.org/10.4230/lipics.ecoop.2024.24openalex-snapshot

Qafny: A Quantum-Program Verifier

inferredcites →https://doi.org/10.4230/lipics.icalp.2021.136openalex-snapshot

Quantum Relational Hoare Logic with Expectations

inferredcites →https://doi.org/10.5281/zenodo.1003420openalex-snapshot

The Coq Proof Assistant

inferredcites →https://doi.org/10.5281/zenodo.15039214openalex-snapshot

Artifact for 'Efficient Formal Verification of Quantum Error Correcting Programs'

inferredcites →https://doi.org/10.5281/zenodo.18067974openalex-snapshot

Engineering Non-Linear Decay Dynamics: Pulse-Level Control and Software-Defined Qubit Rescue on Superconducting Processors

inferredcites →https://doi.org/10.5281/zenodo.3999478openalex-snapshot

Mathematical Components

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.1007/978-3-032-09303-5_7openalex-snapshot

Verification Paradigms for Quantum Computing

inferred← citeshttps://doi.org/10.1007/978-3-032-15700-3_3openalex-snapshot

Efficiently Verifying Quantum Programs with Few T Gates

inferred← citeshttps://doi.org/10.1145/3776658openalex-snapshot

An Expressive Assertion Language for Quantum Programs

inferred← citeshttps://doi.org/10.1145/3776712openalex-snapshot

Parameterized Verification of Quantum Circuits

inferred← citeshttps://doi.org/10.1145/3786582.3786813openalex-snapshot

QSolver: A Quantum Constraint Solver

inferred← citeshttps://doi.org/10.1145/3808314openalex-snapshot

Hybrid Path-Sums for Hybrid Quantum Programs

inferred← citeshttps://doi.org/10.22331/q-2026-07-23-2172openalex-snapshot

Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs

inferred← citeshttps://doi.org/10.32388/h7d715openalex-snapshot