Inductive Approach to Spacer - PLDI 2024

Explore an innovative approach to understanding and improving the Spacer algorithm for solving constrained Horn clause satisfiability problems in this 18-minute video presentation from PLDI 2024. Delve into the research by Takeshi Tsukada and Hiroshi Unno, who propose a novel inductive method to formulate and analyze Spacer-like procedures. Discover how this approach nearly unifies Spacer and GPDR, revealing their key differences. Learn about the challenges in Spacer's refutational completeness and how the inductive perspective helps identify and address these issues. Gain insights into the experimental implementation of the proposed procedure and its evaluation. This talk is essential for researchers and practitioners interested in automated verification methods, constrained Horn clause solving, and the advancement of program analysis techniques.