CHC Model Validation with Proof Guarantees

This document is a research article that presents a two-layered validation approach for constrained Horn clause (CHC) models. The authors, Rodrigo Otoni and colleagues, outline the importance of validating the results of logic solvers, particularly in the context of CHC, which has seen extensive practical usage but limited validation efforts. The proposed approach utilizes a proof-producing SMT solver to validate CHC models through a series of SMT queries, followed by a proof checker to confirm the results of the SMT solver. The authors developed a modular evaluation framework named ATHENA to assess the approach's viability, conducting large-scale experiments that compared various CHC solvers, SMT solvers, and proof checkers. The findings indicate that the validation approach is feasible and highlights the necessity for such validations, as several bugs were identified in the tools used during the evaluation. The document details the methodology, framework, and results of the evaluation, contributing to the field of formal verification.