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

Description in English
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.

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

Key words in English
Formal Verification, Low Level-programming, Separation logic

Czech

Rogalewicz Adam, doc. Mgr., Ph.D. - principal person responsible
Dacík Tomáš, Ing. - fellow researcher
Valko Roderik, MSc - fellow researcher
Vojnar Tomáš, prof. Ing., Ph.D. - fellow researcher

Department of Intelligent Systems
- responsible department (25.9.2025 - not assigned)
Automata@FIT
- internal (25.9.2025 - 31.12.2026)
Automated Analysis and Verification Research Group - VeriFIT
- internal (25.9.2025 - 31.12.2026)
Vienna University of Technology
- co-beneficiary (25.9.2025 - 31.12.2026)
Department of Intelligent Systems
- beneficiary (25.9.2025 - 31.12.2026)

Responsibility: Rogalewicz Adam, doc. Mgr., Ph.D.