Tools

An automata-based verifier for quantum circuits and programs. Sets of quantum states are represented as tree automata, which lets a circuit be checked against a pre-/post-condition specification — or searched for bugs — without enumerating individual states.

Introduced in AutoQ: An Automata-based Quantum Circuit Verifier (CAV’23) and An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits (PLDI’23), then extended with level-synchronized tree automata (POPL’25), verification of quantum programs (TACAS’25) and a practical specification language (CAV’26).

An MTBDD-based quantum circuit simulator. It uses symbolic execution together with loop summarization, so that a repeated block of gates is analysed once rather than unrolled.

Introduced in Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization (ICCAD’24).

An in-browser visualizer for the MTBDD of a pure quantum state — the same representation Medusa computes with. It applies a unitary circuit gate by gate and redraws the decision diagram, picking out the nodes each gate created, so what the structure costs is visible: a uniform superposition over 8 qubits is one node, a 5-qubit GHZ state is 11, and a 3-qubit QFT shares nothing and grows as large as the state vector.

Amplitudes are exact, in the ring Z[1/√2, i] extended with free symbols, so nothing is rounded and two states are equal precisely when their diagrams are the same node. It runs as a single HTML file with no install and no server; the source is on GitHub.