Memory-Safety Verification of Open Programs with Angelic Assumptions

Watch this 12-minute conference presentation from OOPSLA 2025 that introduces Seeker, a novel verification tool for memory-safety analysis of open programs where complete source code is unavailable. Learn how researchers from IIT Kanpur and Microsoft Research address the challenge of excessive false positives in program verification by developing a technique that makes angelic assumptions about missing code components. Discover how the system combines large language model-based mining of idiomatic patterns in buffer-manipulating programs with formal synthesis strategies that perform property-directed reasoning to select and adapt these patterns into verification assumptions. Explore the methodology that guarantees programs are deemed correct only when verified under well-defined trusted idiomatic patterns, and examine experimental results showing Seeker's ability to identify 79% of false positives with zero false negatives across benchmarks from popular open-source software. Gain insights into how this approach distinguishes between genuine bugs and spurious warnings in memory-safety verification, potentially reducing the time-consuming and error-prone process of manually building models for missing code in real-world verification scenarios.