QUAK: Quantum Program Analysis using Automata Toolkit

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

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ň.