Horn-ICE Learning for Synthesizing Invariants and Contracts

TL;DR

This paper introduces Horn-ICE learning algorithms that efficiently synthesize invariants and contracts for program verification by leveraging Horn clauses and decision-tree models, demonstrating practical effectiveness.

Contribution

It presents a novel Horn-ICE learning framework with a polynomial-time decision-tree algorithm for invariant synthesis, extending ICE-learning to Horn clauses.

Findings

Successfully learned invariants for sequential programs

Efficiently synthesized contracts for concurrent programs

Demonstrated robustness and practicality of the approach

Abstract

We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision-tree learning algorithm that learns from Horn-ICE samples, works in polynomial time, and uses statistical heuristics to learn small trees that satisfy the samples. Since most verification proofs can be modeled using Horn clauses, Horn-ICE learning is a more robust technique to learn inductive annotations that prove programs correct. Our experiments show that an implementation of our algorithm is able to learn adequate inductive invariants and contracts efficiently for a variety of sequential and concurrent programs.