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

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.