Learning Invariants using Decision Trees

TL;DR

This paper introduces a decision tree-based algorithm for inferring program invariants by classifying reachable states, demonstrating its effectiveness on challenging C program benchmarks and outperforming other machine learning methods.

Contribution

The paper presents a novel decision tree algorithm for learning Boolean invariants from program states, improving scalability and effectiveness over existing ML-based approaches.

Findings

Successfully infers invariants for complex C programs

Scales well to large sample sets

Outperforms other ML-based invariant inference techniques

Abstract

The problem of inferring an inductive invariant for verifying program safety can be formulated in terms of binary classification. This is a standard problem in machine learning: given a sample of good and bad points, one is asked to find a classifier that generalizes from the sample and separates the two sets. Here, the good points are the reachable states of the program, and the bad points are those that reach a safety property violation. Thus, a learned classifier is a candidate invariant. In this paper, we propose a new algorithm that uses decision trees to learn candidate invariants in the form of arbitrary Boolean combinations of numerical inequalities. We have used our algorithm to verify C programs taken from the literature. The algorithm is able to infer safe invariants for a range of challenging benchmarks and compares favorably to other ML-based invariant inference techniques. In particular, it scales well to large sample sets.