This project addresses the challenges of verifying low-level programs that usepointers and dynamic data structures, where memory-safety errors can lead tosevere reliability and security risks. Building on the prototype tool Broom,developed jointly by the Czech and Austrian teams, we will advance separationlogic-based bi-abductive analysis to improve support for type recasting andscalability. Our research will develop new formal foundations, prove thesoundness of the proposed techniques, and implement prototypes. Through jointwork, we will combine Austrian expertise in decision procedures with Czechexpertise in low-level code analysis, ensuring both scientific progress andtraining of young researchers.