SPLASH 2020 (series) / NSAD 2020 (series) / NSAD 2020 /
Proving array properties using data abstraction
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.
We study the case of arrays and our experimental evaluation show promising results on classical array programs.
Tue 17 NovDisplayed time zone: Central Time (US & Canada) change
Tue 17 Nov
Displayed time zone: Central Time (US & Canada) change
03:00 - 04:20 | PapersNSAD at SPLASH-IV Chair(s): Liqian Chen National University of Defense Technology, China, Khalil Ghorbal Inria, France | ||
03:00 20mPaper | Abstract Domains for Constraint Programming with Differential Equations NSAD Ghiles Ziat , Olivier Mullier , Julien Alexandre dit Sandretto , Christophe Garion ISAE-SUPAERO, Alexandre Chapoutot , Xavier Thirioux | ||
03:20 20mPaper | Numeric Domains Meet Algebraic Data Types NSAD Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Thomas P. Jensen INRIA Rennes, Benoît Montagu Inria | ||
03:40 20mPaper | Proving array properties using data abstraction NSAD | ||
04:00 20mPaper | Rigorous Linear Programming Techniques for Numerical Abstract Domains NSAD | ||