Automating induction for solving horn clauses

Abstract

Verification problems of programs in various paradigms can be reduced to problems of solving Horn clause constraints on predicate variables that represent unknown inductive invariants. This paper presents a novel Horn constraint solving method based on inductive theorem proving: the method reduces Horn constraint solving to validity checking of first-order formulas with inductively defined predicates, which are then checked by induction on the derivation of the predicates. To automate inductive proofs, we introduce a novel proof system tailored to Horn constraint solving, and use a PDR-based Horn constraint solver as well as an SMT solver to discharge proof obligations arising in the proof search. We prove that our proof system satisfies the soundness and relative completeness with respect to ordinary Horn constraint solving schemes. The two main advantages of the proposed method are that (1) it can deal with constraints over any background theories supported by the underlying SMT solver, including nonlinear arithmetic and algebraic data structures, and (2) the method can verify relational specifications across programs in various paradigms where multiple function calls need to be analyzed simultaneously. The class of specifications includes practically important ones such as functional equivalence, asso-ciativity, commutativity, distributivity, monotonicity, idempotency, and non-interference. Our novel combination of Horn clause constraints with inductive theorem proving enables us to naturally and automatically axiomatize recursive functions that are possibly non-terminating, nondeterministic, higher-order, exception-raising, and over non-inductively defined data types. We have implemented a relational verification tool for the OCaml functional language based on the proposed method and obtained promising results in preliminary experiments.