Data-driven Verification of Procedural Programs with Integer Arrays

TL;DR

This paper introduces a data-driven method for verifying procedural programs with integer arrays by synthesizing invariants and pre/post-conditions using decision tree learning, demonstrating efficiency on benchmarks.

Contribution

It extends the decision tree Horn-ICE framework to handle arrays and provides a novel classification-based approach for invariant synthesis.

Findings

Method is efficient and competitive on benchmarks.

Successfully synthesizes invariants for array-manipulating programs.

Outperforms some existing verification tools.

Abstract

We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We propose a new algorithmic method for synthesizing loop invariants and procedure pre/post-conditions represented as universally quantified first-order formulas constraining the array elements and program variables. We adopt a data-driven approach that extends the decision tree Horn-ICE framework to handle arrays. We provide a powerful learning technique based on reducing a complex classification problem of vectors of integer arrays to a simpler classification problem of vectors of integers. The obtained classifier is generalized to get universally quantified invariants and procedure pre/post-conditions. We have implemented our method and shown its efficiency and competitiveness w.r.t. state-of-the-art tools on a significant benchmark.