Proving array properties using data abstraction

International audienceThis paper presents a framework to abstract data structures within Horn clauses that allows abstractions to be easily expressed, compared, composed and implemented. These abstractions introduce new quantifiers that we eliminate with quantifier elimination techniques. Experimental evaluation show promising results on classical array programs