About |QuantumFIT⟩
|QuantumFIT⟩ is the Quantum Computing Systems research group at the Faculty of Information Technology, Brno University of Technology, working on quantum computing and quantum software engineering.
Our work applies formal methods to quantum computing. The recurring idea is to represent whole sets of quantum states symbolically, as tree automata, rather than enumerating states one at a time: a question about a quantum circuit then becomes a question about automata. That makes it possible to check a circuit against a pre-/post-condition specification, or to search it for bugs, without ever enumerating individual states. The same perspective extends from circuits to quantum programs, and to families of circuits rather than single instances.
Alongside verification we work on simulation, using symbolic execution over multi-terminal binary decision diagrams together with loop summarization, so that a repeated block of gates is analysed once instead of being unrolled. Underneath both sits the automata and logic the methods are built from: tree automata and their level-synchronized extension, omega-automata, and logic and SMT solving.
Two tools carry this into practice — AutoQ, a verifier for quantum circuits and programs, and Medusa, a simulator — and the results behind them appear in our publications, at PLDI, POPL, CAV, TACAS and ICCAD.
Contact
Contact person
Postal address
Faculty of Information Technology
Brno University of Technology
Božetěchova 2
612 00 Brno
Czech Republic