Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 13-minute conference presentation from OOPSLA 2025 that introduces two novel proof systems for locating the source of programming errors through backward under-approximation analysis. Learn about Sufficient Incorrectness Logic (SIL) and its specialized variant Separation SIL, designed specifically for handling memory errors in programs with pointers and dynamic memory allocation. Discover how these proof systems address the limitations of traditional sound over-approximation methods that produce false alarms by focusing on bug detection without false positives. Examine the theoretical foundations of SIL as a minimal, sound, and complete system for Lisbon triples, enabling detailed comparison of triple-based program logics across dimensions including negation, approximation, execution order, and analysis objectives. Understand the technical contributions of Separation SIL as a sound and relatively complete proof system for automated backward reasoning, with completeness results achieved through careful crafting of both assertion language and inference rules for atomic commands. Gain insights into how these approaches can help programmers more effectively identify and address memory-related bugs in their code by tracing errors back to their sources rather than simply detecting their presence.
