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
03:00 - 04:20
|Abstract Domains for Constraint Programming with Differential Equations
|Numeric Domains Meet Algebraic Data Types
|Proving array properties using data abstraction
|Rigorous Linear Programming Techniques for Numerical Abstract Domains