An encoding of array verification problems into array-free Horn clauses

David Monniaux, Laure Gonnord

Automatically verifying safety properties of programs is hard, and it is even harder if the program acts upon arrays or other forms of maps. Many approaches exist for verifying pro…