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.