Under-approximation for Scalable Bug Detection

Explore a keynote presentation on under-approximation techniques for scalable bug detection in software development. Delve into Incorrectness Logic (IL) and its dual relationship with Hoare Logic, understanding how IL proves the presence of bugs rather than their absence. Learn about Incorrectness Separation Logic (ISL), which combines IL's under-approximate reasoning with separation logic's local reasoning to enable compositional and scalable bug detection. Discover Pulse-X, an automatic program analysis tool based on ISL, and its practical applications in finding memory safety errors in large codebases like OpenSSL. Compare Pulse-X's performance against state-of-the-art tools and gain insights into its effectiveness in real-world scenarios. This 59-minute video, presented by Azalea Raad at the CPP 2024 conference, offers valuable knowledge for software developers, researchers, and anyone interested in advanced bug detection methodologies.