Automating Induction for Solving Horn Clauses

TL;DR

This paper introduces a new method for solving Horn clause constraints using inductive theorem proving, enabling automated verification of complex relational properties across various programming paradigms.

Contribution

It presents a novel Horn constraint solving approach based on inductive theorem proving, with a tailored proof system and SMT integration, applicable to diverse program specifications.

Findings

Successfully verified relational properties like functional equivalence and non-interference.

Implemented a tool for OCaml that shows promising preliminary results.

Enables reasoning about non-terminating, non-deterministic, and higher-order recursive functions.

Abstract

Verification problems of programs written in various paradigms (such as imperative, logic, concurrent, functional, and object-oriented ones) 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 an SMT solver to discharge proof obligations arising in the proof search. The main advantage of the proposed method is that it 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, associativity, commutativity, distributivity, monotonicity, idempotency, and non-interference. Furthermore, 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, non-deterministic, 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.