About |QuantumFIT⟩

|QuantumFIT⟩ is a research group at the Faculty of Information Technology, Brno University of Technology, bringing together researchers and students interested in studying quantum computing systems in a broad range. The main aim of the group is to empower the transition from today’s noisy, small-scale quantum devices to machines delivering a practical quantum advantage, by developing the algorithmic foundations and the software tools needed to design quantum computations, analyse them, and make their results trustworthy.

The group builds on a strong background in formal methods, automated reasoning, and automata theory, and transfers these techniques into the quantum domain. These foundations are also an object of study in their own right: the group works on automata models and on logical theories and their decision procedures, together with the questions of decidability, complexity, and succinctness that decide what a formalism can deliver in practice. Within the quantum domain, a substantial part of the work targets the representations themselves: models for representing sets of quantum states and quantum operations, in particular automata models and decision diagram models, together with their canonical forms and the algorithms over them; decision procedures based on SAT/SMT solving; and rigorous semantics of quantum circuits and programs. On these foundations the group develops prototype tools, in particular simulators, optimizers, verifiers, synthesis engines, and tools supporting the design of quantum error-correcting codes. The same foundations also make it possible to go beyond analysing existing computations and to design new ones: quantum algorithms and trusted building blocks such as quantum arithmetic, oracles, and primitives for state preparation and uncomputation, which come with correctness guarantees and a known resource cost and can be reused as reliable components of larger quantum computations. Besides basic research, the group also contributes to the infrastructure of the wider community, for instance to benchmark collections that make the resulting tools comparable.

Research Focus

Analysis, verification, optimization, and synthesis of quantum circuits and programs, together with the underlying foundations of automated reasoning, automata theory, and logic, which the group studies both for their own sake and as the machinery its quantum tools are built on, including:

• Foundations: automata models and logical theories — studied as objects in their own right, together with the algorithms and decision procedures over them and the decidability, complexity, and succinctness results that delimit what such formalisms can do.
• Formal models and representations — automata models and decision diagram models for sets of quantum states and for quantum operations, their canonical forms, normalization and closure properties, the complexity and lower bounds of such representations, and formal semantics of quantum circuits and programs.
• Simulation of quantum circuits and programs — scalable symbolic and semi-symbolic simulation techniques based on decision diagrams, aimed at both near-term (NISQ) and fault-tolerant workloads.
• Verification and equivalence checking — automated reasoning about the equivalence of quantum circuits, their correctness with respect to a specification, and properties of quantum programs, using decision procedures, model checking, and automata-based representations of sets of quantum states.
• Optimization and compilation — reducing the resource cost of quantum computation (gate count, T-count and T-depth, circuit depth, number of qubits, ancilla usage), fault-tolerant compilation and resource estimation, and hardware-aware mapping and routing onto concrete devices.
• Synthesis of quantum circuits — exact and approximate synthesis driven by solvers (SAT, SMT, #SAT, QBF) and by search, including synthesis over restricted and hardware-native gate sets and of probabilistic constructions such as repeat-until-success circuits.
• Quantum algorithms and trusted building blocks — design of new quantum algorithms and of reusable, resource-efficient circuit primitives (quantum arithmetic, oracles, multi-controlled operations, state preparation, measurement-based uncomputation) whose correctness and resource cost are established rigorously, so that they can serve as trusted components of larger computations.
• Quantum error correction — techniques and tools supporting the design, analysis, and evaluation of quantum error-correcting codes and their decoders, together with an assessment of the overhead that fault-tolerant execution imposes.
• Benchmarks and community infrastructure — benchmark suites, input/output formats, and competitions of tools for automated reasoning over quantum circuits, enabling a fair and reproducible comparison of the approaches developed in the field.

Contact