[PLDI24] Inductive Approach to Spacer

Описание: Inductive Approach to Spacer (Video, PLDI 2024)
Takeshi Tsukada and Hiroshi Unno
(Chiba University, Japan; Tohoku University, Japan)

Abstract: The constrained Horn clause satisfiability problem is at the core of many automated verification methods, and Spacer is one of the most efficient solvers of this problem. The standard description of Spacer is based on an abstract transition system, dividing the whole procedure into small rules. This division makes individual rules easier to understand but, conversely, makes it difficult to discuss the procedure as a whole. As evidence of the difficulty in understanding the whole procedure, we point out that the claimed refutational completeness actually fails for several reasons, some of which were not present in the original version and subsequently added. It is also difficult to grasp the differences between Spacer and another procedure, such as GPDR.
This paper aims to provide a better understanding of Spacer by developing a Spacer-like procedure defined by structural induction. We first formulate the problem to be solved inductively, then give its naïve solver and transform it to obtain a Spacer-like procedure. Interestingly, our inductive approach almost unifies Spacer and GPDR, which differ in only one respect in our understanding. To demonstrate the usefulness of our inductive approach in understanding Spacer, we examine Spacer variants in the literature in terms of inductive procedures and discuss why they are not refutationally complete and how to fix them. We also implemented the proposed procedure and evaluated it experimentally.

Article: https://doi.org/10.1145/3656457

Supplementary web page: https://github.com/hiroshi-unno/coar

ORCID: https://orcid.org/0000-0002-2824-8708, https://orcid.org/0000-0002-4225-8195

Video Tags: constrained Horn clause, model-based projection, tree interpolation, refutational completeness, pldi24main-p738-p, doi:10.1145/3656457, orcid:0000-0002-2824-8708, orcid:0000-0002-4225-8195

Presentation at the PLDI 2024 conference, June 24–28, 2024, https://pldi24.sigplan.org/
Sponsored by ACM SIGPLAN,