Detail projektu
QUAK: Quantum Program Analysis using Automata Toolkit
Období řešení: 1. 1. 2025 – 31. 12. 2027
Typ projektu: grant
Kód: GA25-18318S, 25-18318S
Agentura: Grantová agentura České republiky
Program: Standardní projekty
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ň.
Češka Milan, doc. RNDr., Ph.D. (UITS)
Havlena Vojtěch, Ing., Ph.D. (UITS)
Havlík Jakub (UITS)
Hečko Michal, Ing. (UITS)
Hudák David, Ing. (UITS)
Macák Filip, Ing. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Síč Juraj, Mgr. (UITS)
Vašíček Ondřej, Ing. (UITS)
2025
- HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O. Negated String Containment is Decidable. Leibniz International Proceedings in Informatics. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2025.
p. 1. Detail - HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementation of Emerson-Lei Automata. Proceedings of FoSSaCS'25. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2025. iss. 1,
p. 88. ISSN: 0302-9743. Detail - CHEN, Y.; HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O. A Uniform Framework for Handling Position Constraints in String Solving. Proceedings of the ACM on Programming Languages-PACMPL, 2025, vol. 9, iss. PLDI,
p. 550-575. ISSN: 2475-1421. Detail - LENGÁL, O.; CHEN, Y.; LIN, J.; TSAI, W.; HSIEH, M.; HUANG, W.; CHUNG, K. AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs. In Proceedings of TACAS'25. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2025. iss. 15698,
p. 87-108. ISSN: 0302-9743. Detail