A Comparison of Program Logics for (In)Correctness

Explore a comprehensive comparison of program logics for correctness and incorrectness in this 31-minute conference talk from ACM SIGPLAN. Delve into the evolution of formal methods for guaranteeing program properties, from Floyd and Hoare's pioneering work to modern techniques. Examine the concepts of over-approximation and under-approximation in program analysis, understanding their roles in ensuring correctness and identifying bugs. Classify various program logics based on their approximation methods and investigate the relationships between them. Gain insights into the fundamental differences between over- and under-approximation approaches. Discover a novel logic for backward under-approximation, including the introduction of Sufficient Incorrectness Logic (SIL) and its sound and complete proof system. Learn about Separation SIL, an extension of the concept to handle dynamic heap management using Separation Logic principles.