Tools

AutoQ

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).

Medusa

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).