Data-driven Verification of Procedural Programs with Integer Arrays

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.

@article{bouajjani2025_2505.15958,
  title={ Data-driven Verification of Procedural Programs with Integer Arrays },
  author={ Ahmed Bouajjani and Wael-Amine Boutglay and Peter Habermehl },
  journal={arXiv preprint arXiv:2505.15958},
  year={ 2025 }
}