Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique.

翻译：约束Horn子句（CHCs）传统上被用作形式验证中的低级表示。现有求解器大多采用多种专门技术，包括直接状态空间遍历或下近似抽象，这需要构建专用复杂算法。另一些求解器通过将问题转化为其他验证任务的输入，成功简化了验证流程，从而利用现有算法的优势。其中一种方法将CHC问题转化为近似模拟演绎任务的递归程序，并验证指定为控制位置的安全违规的可达性。我们针对线性CHCs提出了一种替代的自底向上方法，并在开源模型检查框架THETA上对合成示例与工业实例进行了两种方案的评估。我们发现，相较于自顶向下技术，在验证流程中采用新型自底向上方法时，可解决问题的数量提升了两倍以上。