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