Syntéza pravděpodobnostních programů

Předmětem disertační práce bude zejména vývoj teoretických základů pro nové škálovatelné metody syntézy pravděpodobnostních programů. Zaměříme se na využití syntézy řízené syntaxí a na dosud neprozkoumanou oblast spojení pokročilých metod formální kvantitativní analýzy s přístupy založenými na SAT/SMT, prohledávání stavového prostoru a technikami induktivní syntézy. Práce se rovněž zaměří na využití těchto metod v procesu návrhu prakticky relevantních pravděpodobnostních systémů, a na důkladné vyhodnocení aplikovatelnosti těchto metod. Výsledky této práce přispějí k pokroku v oblasti automatizace návrhu systémů.

Výzkumu efektivních metod syntézy je v současnosti věnována značná pozornost v oblastech formální verifikace, návrhu a implementace programovacích jazyků, umělé inteligence a systémové biologie, o čemž svědčí zaměření řady špičkových konferencí (např. CAV, TACAS, PLDI či CMSB). Syntézou programů a modelů se rovněž zabývá řada velkých projektů na špičkových universitách a výzkumných institucích (např. Berkeley University či Microsoft Research).

Práce bude řešena ve spolupráci s týmem VeriFIT pod vedením doc. M. Češky jr. Dále se počítá s úzkou spoluprací se skupinou prof. J.P. Katoena (řešitel ERC Advanced grantu) z RWTH Aachen University (Německo) a se skupinou assoc. prof. N. Jansena (řešitel ERC Starting grantu) z Radboud University Nijmegen (Nizozemí).  

V případě zodpovědného přístupu a kvalitních výsledků je zde možnost zapojení do grantových projektů (např. české projekty GAČR či evropské projekty Horizone Europe).