4 papers · 1 filter
Generalized LIMDDs: Succinctness and Canonicity for Decision Diagrams Modulo a Group
Arend-Jan Quist, Alexis de Colnet, Thomas Reps +1
A reduced ordered decision diagram is the minimal automaton of a function on words of fixed length: its nodes are the residuals, and reduction is the Myhill--Nerode quotient. We st…
Manjushri: A Tool for Equivalence Checking of Quantum Circuits
Xuan Du Trinh, Meghana Sistla, Nengkun Yu +1
Verifying whether two quantum circuits are equivalent is a central challenge in the compilation and optimization of quantum programs. We introduce \textsc{Manjushri}, a new automat…
SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
Nengkun Yu, Jens Palsberg, Thomas Reps
Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Despite extensive research, existing verification t…
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Nengkun Yu, Xuan Du Trinh, Thomas Reps
This paper concerns the problem of checking if two shallow (i.e., constant-depth) quantum circuits perform equivalent computations. Equivalence checking is a fundamental correctnes…