Inductive Approach to Spacer

The constrained Horn clause satisfiability problem is at the core of many automated verification methods, and S pacer is one of the most efficient solvers of this problem. The standard description of S pacer 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 S pacer and another procedure, such as GPDR. This paper aims to provide a better understanding of S pacer by developing a S pacer -like procedure defined by structural induction. We first formulate the problem to be solved inductively, then give its naive solver and transform it to obtain a S pacer -like procedure. Interestingly, our inductive approach almost unifies S pacer and GPDR, which differ in only one respect in our understanding. To demonstrate the usefulness of our inductive approach in understanding S pacer , we examine S pacer 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.