# Data-driven Verification of Procedural Programs with Integer Arrays

arXiv: https://arxiv.org/abs/2505.15958 · HTML: https://mlsanity.com/paper/2505.15958/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 57 references that are in the map.
- First posted on arXiv 21 May 2025.

## Builds on (most cited first, 14 of 14)

- [SMT-based Model Checking for Recursive Programs](https://mlsanity.com/paper/1405.4028/) (2014)
- [Horn-ICE Learning for Synthesizing Invariants and Contracts](https://mlsanity.com/paper/1712.09418/) (2017)
- [Overfitting in Synthesis: Theory and Practice (Extended Version)](https://mlsanity.com/paper/1905.07457/) (2019)
- [Diffy: Inductive Reasoning of Array Programs using Difference Invariants](https://mlsanity.com/paper/2105.14748/) (2021)
- [Learning Universally Quantified Invariants of Linear Data Structures](https://mlsanity.com/paper/1302.2273/) (2013)
- [Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays](https://mlsanity.com/paper/2101.06825/) (2021)
- [Horn Clauses as an Intermediate Representation for Program Analysis and Transformation](https://mlsanity.com/paper/1507.05762/) (2015)
- [Verifying Relational Properties using Trace Logic](https://mlsanity.com/paper/1906.09899/) (2019)
- [Verifying Array Manipulating Programs with Full-Program Induction](https://mlsanity.com/paper/2002.09857/) (2020)
- [Trace Logic for Inductive Loop Reasoning](https://mlsanity.com/paper/2008.01387/) (2020)
- [Quantifiers on Demand](https://mlsanity.com/paper/2106.00664/) (2021)
- [The VMT-LIB Language and Tools](https://mlsanity.com/paper/2109.12821/) (2021)
- [Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes](https://mlsanity.com/paper/2205.14943/) (2022)
- [Invariant Checking for SMT-based Systems with Quantifiers](https://mlsanity.com/paper/2402.19028/) (2024)

## Abstract (arXiv)

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.