Pokročilá analýza a verifikace pro pokročilý software

Obecným cílem výzkumu v rámci zadání je výrazně posunout vpřed současný stav poznání ve světě v oblasti statické analýzy a verifikace s formálními kořeny se zaměřením na analýzu a verifikaci pokročilého software, a to jak v oblasti principů, tak i nástrojů alespoň potenciálně využitelných v praxi.

Statická analýza a verifikace na formálních základech představují moderní a rychle se rozvíjející přístupy k ověřování korektnosti počítačových systémů, resp. pro vyhledávání chyb v nich. Existuje a dále se rozvíjí mnoho přístupů k takové analýze či verifikaci: analýza toku dat, pokročilé typové analýzy, abstraktní interpretace, model checking apod. Značná pozornost je těmto přístupům věnována nejen v akademické oblasti, ale také řadou špičkových velkých průmyslových společností (např. Meta, Google, Amazon, Apple, Microsoft, Oracle, Red Hat, Honeywell apod.) i neustále vznikajících specializovaných firem (např. Coverity, GrammaTech, AbsInt, DiffBlue, Certora apod.), často následně zakoupených velkými technologickými leadery. 

Přes výše uvedený zájem univerzit i průmyslových společností je však v oblasti statické analýzy stále zapotřebí vyřešit celou řadu teoretických i praktických problémů. Zvlášť patrné je to u analýzy a verifikace pokročilého software, založeného na nízko-úrovňovém programování, moderních vysoko-úrovňových přístupech či obojím. Z hlediska analýzy a verifikace jsou problematické mezi nízko-úrovňovými programy stále např. programy využívající nízko-úrovňovou manipulaci s ukazateli a dynamickými datovými strukturami, zatímco mezi vysoko-úrovňové programy se jedná např. o programy využívající strojové učení či založené na expertních systémech (vyvíjené např. ve společnosti Honeywell), vysoko-úrovňové specifikace software či programy v moderních vysoko-úrovňových jazycích a prostředích (např. Oracle GraalVM) a/nebo využívající moderní architektury software, jako jsou např. mikroslužby. V rámci výzkumu se student bude moci postupně specializovat na verifikační problémy v některé z těchto oblastí. Rozvíjeny budou přístupy založené na různých formách logik a automatů, abstraktní interpretaci, abdukci, symbolické exekuci či jejich vhodných kombinacích.

Práce bude řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou analýzou a verifikací, zejména pak doc. A. Rogalewiczem, dr. J. Fiedorem, doc. L. Holíkem, dr. O. Lengálem, Ing. V. Malíkem, Ing. J. Pavelou, Ing. O. Vašíčkem či Ing. D. Kozákem. Je zde rovněž možnost úzké spolupráce s různými zahraničními partnery VeriFIT -- zejména TU Vídeň (doc. F. Zuleger) a University of Arizona (dr. T. Černý), případně Uppsala University (prof. P.A. Abdulla); Verimag, Grenoble (doc. R. Iosif), IRIF, Paříž (prof. A. Bouajjani, doc. P. Habermehl), LSV, ENS Paris-Saclay (prof. M. Sighireanu), Academia Sinica, Tchaj-wan (prof. Y.-F. Chen). Téma je zajímavé také z pohledu spolupráce s průmyslovými společnostmi, zejména pak Red Hat (spolupráce V. Malík), Honeywell (spolupráce J. Fiedor, T. Kratochvíla, J. Pavela, O. Vašíček), Oracle Labs (spolupráce D. Kozák).

V oblasti statické analýzy programů dosáhla skupina VeriFIT mnoha originálních výsledků publikovaných na špičkových konferencích. Řada z dosažených výsledků byla implementována v nástrojích (např. Predator, Forester, 2LS), které získaly řadu ocenění např. na mezinárodní soutěži ve verifikaci software SV-COMP. V nedávné době začali členové skupiny vyvíjet také