Horn-ICE Learning for Synthesizing Invariants and Contracts
This work addresses the challenge of automated program verification for developers and researchers, offering a more robust technique for learning inductive annotations, though it is incremental as it builds upon the existing ICE-learning model.
The paper tackles the problem of synthesizing invariants and contracts for program verification by introducing Horn-ICE learning, an extension of the ICE-learning model, and presents a decision-tree learning algorithm that operates in polynomial time and uses statistical heuristics to produce small trees. The experiments demonstrate that the implementation efficiently learns adequate inductive invariants and contracts for various sequential and concurrent programs.
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.