2025/05/21 by Ahmed Bouajjani, Bouajjani, Ahmed, Wael-Amine Boutglay +3 · 1 citation
Computer Science · #Evolutionary Algorithms and Applications #FOS: Computer and information sciences #Formal Methods in Verification #Machine Learning (cs.LG) #Machine Learning and Data Classification #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2505.15958
openalex publication_date 2025/05/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.