Data-driven Verification of Procedural Programs with Integer Arrays

Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl

We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We pro…