AutoQ is a command-line utility written in C++ for verifying partial correctness of quantum programs automatically based on non-deterministic finite tree automata (NFTA) along with the concept of Hoare-style proof systems.
Consider a triple {
Our program currently supports
Currently, for Linux (Ubuntu/Debian) and macOS, the dependency of AutoQ can be built using the command ./configure.sh
. After configuration, please run the following command.
make release
make test
The first command compiles the source code with compiler optimizations enabled, while the second command runs several unit tests to verify the correctness of the implementation. If you need to compile the library for debugging, you can replace make release with make debug
.
There are 5 modes listed in the following help message, which can be accessed by typing their respective subcommands. Each mode (subcommand) also has its own usage instructions.
$ ./build/cli/autoq -h
AutoQ: An automata-based C++ tool for quantum program verification.
Usage: autoq [OPTIONS] [SUBCOMMAND]
Options:
-h,--help Print this help message and exit
Subcommands:
exC Concrete Execution
verC Concrete Verification
exS Symbolic Execution
verS Symbolic Verification
eq Equivalence Checking
$ ./build/cli/autoq verC benchmarks/Grover/03/pre.spec benchmarks/Grover/03/circuit.qasm benchmarks/Grover/03/post.spec
The quantum program has [6] qubits and [54] gates.
The verification process [passed] in [0.0s] with [16MB] memory usage.
AutoQ provides two file extensions, *.hsl and *.spec, for users to indicate the format they use to describe a set of quantum states. The simpler format is *.hsl, which does not require users to have a background in NFTA. However, since our current implementation of *.hsl has not yet been optimized, we strongly recommend using *.spec as the number of qubits increases. The detailed formats can be found in the following documents.
If you're interested in the internal structures for quantum state representation, see the file internal_structure.md.