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.