Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Data-driven Verification of Procedural Programs with Integer Arrays

Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl

TL;DR

The paper tackles automatic verification of procedural programs that manipulate parametric-size integer arrays by encoding verification conditions as constrained Horn clauses and synthesizing invariants and pre/post-conditions as universally quantified formulas. It extends the Horn-ICE learning framework with a data-driven, decision-tree-based approach (Horn-ICE-DT) and introduces diagramization to convert array-based CHCs into learnable classification problems, using Z3 as the teacher in an iterative loop. The authors implement this as the Tapis tool and demonstrate improved coverage on a large SV-COMP/TAPIS-Bench benchmark, including recursive procedures, with competitive performance against state-of-the-art tools. The work offers a scalable, data-driven method for inferring quantified invariants and pre/post-conditions for array-manipulating programs, contributing a practical approach to CHC solving in the presence of arrays and recursion.

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.

Data-driven Verification of Procedural Programs with Integer Arrays

TL;DR

The paper tackles automatic verification of procedural programs that manipulate parametric-size integer arrays by encoding verification conditions as constrained Horn clauses and synthesizing invariants and pre/post-conditions as universally quantified formulas. It extends the Horn-ICE learning framework with a data-driven, decision-tree-based approach (Horn-ICE-DT) and introduces diagramization to convert array-based CHCs into learnable classification problems, using Z3 as the teacher in an iterative loop. The authors implement this as the Tapis tool and demonstrate improved coverage on a large SV-COMP/TAPIS-Bench benchmark, including recursive procedures, with competitive performance against state-of-the-art tools. The work offers a scalable, data-driven method for inferring quantified invariants and pre/post-conditions for array-manipulating programs, contributing a practical approach to CHC solving in the presence of arrays and recursion.

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.

Paper Structure

This paper contains 18 sections, 5 theorems, 5 equations, 5 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related work
  3. Programs and Specification
  4. Programs
  5. Specifications
  6. Safety verification
  7. Constrained Horn Clauses (CHC) and CHC solving
  8. Constrained Horn Clauses
  9. Data-driven CHC solving using Horn-ICE
  10. Diagramization
  11. Decision Tree-based Quantified Invariants Learner
  12. The learner
  13. Attribute Discovery
  14. Experiments
  15. Conclusion
  16. ...and 3 more sections

Key Result

theorem 1

Let $\mathcal{S} = (X, C)$ be a consistent data point sample and let $\mathcal{S}'_n = \delta_n(\mathcal{S})$ be the corresponding diagram sample. If $\mathcal{S}'_n$ is consistent and $J'$ is a classifier of $\mathcal{S}'_n$ then $\xi(J')$ is a classifier of $\mathcal{S}$.

Figures (5)

  • Figure 1: The main loop of Horn-ICE.
  • Figure 2: (a) A data point sample which has a classifier and (b) its (non consistent) diagram sample using only one quantifier per array does not admit any classifier.
  • Figure 3: The quantified interpretations learner.
  • Figure 4: Runtime of Tapis vs. Spacer, Prophic3, Vajra, Diffy, UAutomizer and FreqHorn.
  • Figure 5: A program that computes the index of the maximal element of an array (left) using a recursive procedure (right).

Theorems & Definitions (16)

  • definition 1: Parametric-Size Array Property
  • definition 2
  • definition 3
  • definition 4: Data point Sample
  • definition 5: Consistent Labeling of a Data point Sample
  • definition 6: Consistent Data point Sample
  • definition 7: Classifier of a Data point Sample
  • definition 8: Diagram
  • definition 9
  • definition 10
  • ...and 6 more