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

Popis anglicky
This project addresses the challenges of verifying low-level programs that use pointers and dynamic data structures, where memory-safety errors can lead to severe reliability and security risks. Building on the prototype tool Broom, developed jointly by the Czech and Austrian teams, we will advance separation logic-based bi-abductive analysis to improve support for type recasting and scalability. Our research will develop new formal foundations, prove the soundness of the proposed techniques, and implement prototypes. Through joint work, we will combine Austrian expertise in decision procedures with Czech expertise in low-level code analysis, ensuring both scientific progress and training of young researchers.

Klíčová slova
Formální verifikace, Nízkoúrovňové programování, Separační logika

Klíčová slova anglicky
Formal Verification, Low Level-programming, Separation logic

čeština

Rogalewicz Adam, doc. Mgr., Ph.D. - hlavní řešitel
Dacík Tomáš, Ing. - spoluřešitel
Valko Roderik, MSc - spoluřešitel
Vojnar Tomáš, prof. Ing., Ph.D. - spoluřešitel

Ústav inteligentních systémů
- odpovědné pracoviště (25.9.2025 - nezadáno)
Automata@FIT
- interní (25.9.2025 - 31.12.2026)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT
- interní (25.9.2025 - 31.12.2026)
Ústav inteligentních systémů
- příjemce (25.9.2025 - 31.12.2026)

Odpovědnost: Rogalewicz Adam, doc. Mgr., Ph.D.