Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling⋆

Abstract. Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpo-lation, and is proposed as a unifying formalism for expressing abstrac-tion refinement. In abstraction refinement, it is often desirable to infer “simple ” refinements, and researchers have studied techniques for infer-ring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Horn-clause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have imple-mented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.