News
Parameterized verification of quantum circuits accepted at POPL'26
The paper “Parameterized Verification of Quantum Circuits” was accepted at POPL'26 in Rennes, France, to appear in PACMPL 10 (POPL).
Read moreQuantum circuit verification in Communications of the ACM
The paper “An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits” appeared in the June 2025 issue of Communications of the ACM, volume 68 issue 6, pages 85–93.
Read moreQuantum program verification accepted at TACAS'25
The paper “AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs” was accepted at TACAS'25 in Hamilton, Canada. It extends AutoQ from verifying quantum circuits to verifying quantum programs.
Read moreSára Jobranová wins 8 z VUT with quantum circuit simulation
Sára Jobranová won 8 z VUT 2024, the university-wide showcase of the best bachelor’s theses from across all VUT faculties. The jury judged her presentation on quantum circuit simulation the most impressive of the final evening, praising how clearly she put across a difficult topic.
Read moreLevel-synchronized tree automata for quantum circuits accepted at POPL'25
The paper “Verifying Quantum Circuits with Level-Synchronized Tree Automata” was accepted at POPL'25 in Denver, Colorado, to appear in PACMPL 9 (POPL). The level-synchronized automata it introduces extend the class of quantum circuits AutoQ can verify.
Read moreQuantum circuit simulation accepted at ICCAD'24
The paper “Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization” was accepted at ICCAD'24 in New Jersey. It introduces Medusa, which simulates quantum circuits symbolically and analyses a repeated block of gates once rather than unrolling it.
Read moreQuantum circuit verifier AutoQ accepted at CAV'23
The paper “AutoQ: An Automata-based Quantum Circuit Verifier” was accepted at CAV'23 in Paris, France. AutoQ verifies quantum circuits and programs by representing whole sets of quantum states as tree automata, so a circuit can be checked against a specification without enumerating individual states.
Read moreDistinguished Paper Award at PLDI'23 for quantum circuit verification
The paper “An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits” was named a Distinguished Paper at PLDI'23 in Orlando, Florida.
Read moreQuantum circuit verification paper accepted at PLDI'23
The paper “An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits” was accepted at PLDI'23, to appear in PACMPL 7 (PLDI). It checks a quantum circuit against a pre-/post-condition specification, or searches it for bugs, without ever enumerating individual quantum states.
Read more