Quantum computing promises solving problems deemed infeasible for classical computers. While certain problems (e.g. factoring) are known to have fast quantum algorithms, development of quantum algorithms for other problems is extremely challenging due to the complexity of understanding quantum programs and reasoning over them. Existing approaches for their verification, analysis, and simulation are limited in their expressivity, precision, scalability, or require significant manual effort. In the project, we will address these limitations by a) developing new formal models capable of compactly encoding structured (sets of) quantum states that occur in quantum programs, building on ideas from automata theory; b) designing languages for describing pre-/post-conditions in quantum programs that will be easy to use and algorithms for their translation into the formal models; and c) proposing new efficient algorithms for automated reasoning over quantum programs that will, together with the two previous goals, push the capabilities of reasoning over quantum programs to a new level.

Description in Czech
Kvantové počítače slibují řešení problémů, které nelze efektivně řešit klasickými počítači. Zatímco některé problémy (např. faktorizace) jde řešit rychleji kvantovými algoritmy, vývoj kvantových programů pro jiné problémy je extrémně náročný z důvodu složitosti pochopení kvantových programů a usuzování nad nimi. Existující přístupy pro jejich verifikaci, analýzu a simulaci mají omezenou expresivitu, přesnost, škálovatelnost, nebo vyžadují značné manuální úsilí. V tomto projektu se zaměříme na tato omezení prostřednictvím a) vývoje nových formálních modelů schopných kompaktní reprezentace strukturovaných (množin) kvantových stavů vyskytujících se v kvantových programech, založených na teorii automatů; b) návrhu jazyků pro popis vstupních a výstupních podmínek v kvantových programech, které budou jednoduché na použití, a algoritmů pro překlad do formálních modelů a c) vytvoření nových efektivních algoritmů pro automatické usuzování nad kvantovými programy, které, spolu s dvěmi předchozími cíly, posune možnosti usuzování nad kvantovými programy na novou úroveň.

Keywords
quantum algorithms;specification languages;formal models;decision diagrams;tree automata;verification;simulation;analysis;logic

Key words in Czech
kvantové algoritmy;specifikační jazyky;formální modely;rozhodovací diagramy;stromové automaty;verifikace;simulace;analýza;logika