A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)

DOI10.1007/978-3-031-38499-8_10MaRDI QIDQ6492738

Yu-Fang Chen, Philipp Rümmer, Wei-Lun Tsai

Publication date: 26 April 2024

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Model checking quantum Markov chains
• Reasoning about vectors using an SMT theory of sequences
• Model checking QCTL plus on quantum Markov chains
• NP satisfiability for arrays as powers
• Solving and interpolating constant arrays based on weak equivalences
• Weakly Equivalent Arrays
• Quantum Computation and Quantum Information
• Quantum Entanglement Analysis Based on Abstract Interpretation
• A note on succinct representations of graphs
• Interacting quantum observables: categorical algebra and diagrammatics
• Quantum complexity theory
• A Decision Procedure for Bit-Vectors and Arrays
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• A solver for arrays with concatenation
• \textsf{symQV}: automated symbolic verification of quantum programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)