Data-driven Verification of Procedural Programs with Integer Arrays
This addresses verification challenges for programs with arrays, but it is incremental as it extends existing frameworks to handle arrays.
The paper tackles the problem of verifying procedural programs with integer arrays by proposing a data-driven method for synthesizing loop invariants and procedure pre/post-conditions, showing efficiency and competitiveness against state-of-the-art tools on a benchmark.
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.