Pokrok v automatizovaném ověřování nízkoúrovňových programů prostřednictvím separační logiky a bi-abdukce

Tento projekt se zaměřuje na ověřování nízkoúrovňových programů využívajících
ukazatele a dynamické datové struktury, kde chyby v práci s pamětí mohou vést
k vážným problémům spolehlivosti i bezpečnosti. Na základě prototypového nástroje
Broom, vyvinutého společně českým a rakouským týmem, rozvineme bi-abduktivní
analýzu založenou na separační logice s cílem zlepšit podporu přetypování
a škálovatelnost. Výzkum bude zahrnovat tvorbu nových formálních základů, důkaz
správnosti navržených metod a implementaci prototypů. Spojením rakouské expertízy
v oblasti rozhodovacích procedur a české expertízy v analýze nízkoúrovňového kódu
dosáhneme vědeckého pokroku a zároveň zajistíme školení mladých výzkumníků.