Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification

This conference talk explores how gradual verification connects to both overapproximating logics (Hoare logic) and underapproximating logics (incorrectness logic). Discover a novel approach through gradual exact logic that unifies these seemingly disparate verification methods. Learn how researchers Conrad Zimmerman and Jenna DiVincenzo from Northeastern University and Purdue University demonstrate that Hoare logic, incorrectness logic, and gradual verification can all be defined within this unified framework. Understand the potential implications for developing tools and techniques applicable to both gradual verification and bug-finding, leveraging principles from gradual typing. Presented at the Theory and Practice of Static Analysis workshop (TPSA'25) on January 21, 2025, this 16-minute talk sponsored by ACM SIGPLAN offers valuable insights for researchers and practitioners in program verification.