AutoQ: An Automata-Based Quantum Circuit Verifier
Yu‐Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai
Abstract
Abstract We present a specification language and a fully automated tool named AutoQ for verifying quantum circuits symbolically. The tool implements the automata-based algorithm from [14] and extends it with the capabilities for symbolic reasoning. The extension allows to specify relational properties, i.e., relationships between states before and after executing a circuit. We present a number of use cases where we used AutoQ to fully automatically verify crucial properties of several quantum circuits, which have, to the best of our knowledge, so far been proved only with human help.
Topics & Concepts
Computer scienceAutomatonTheoretical computer scienceExtension (predicate logic)QuantumElectronic circuitSymbolic executionQuantum circuitProgramming languageAlgorithmQuantum computerSoftwareQuantum networkEngineeringPhysicsElectrical engineeringQuantum mechanicsQuantum Computing Algorithms and ArchitectureFormal Methods in VerificationMachine Learning and Algorithms