QUAK: Quantum Program Analysis using Automata Toolkit

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

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.