Proving array properties using data abstraction

Julien Braine (1, 2, 3, 4, 5) , Laure Gonnord (1, 2, 3, 4, 5)

1 LIP - Laboratoire de l'Informatique du Parallélisme
2 ENS de Lyon - École normale supérieure de Lyon
3 CNRS - Centre National de la Recherche Scientifique
4 UCBL - Université Claude Bernard Lyon 1
5 CASH - CASH - Compilation and Analysis, Software and Hardware

This 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.

Mots clés: abstraction; data structures; Horn clauses; array properties

Domaines: Informatique [cs]

Julien Braine, Laure Gonnord. Proving array properties using data abstraction. Numerical and Symbolic Abstract Domains (NSAD), Nov 2020, Virtual, United States. ⟨hal-02948081v2⟩