Proving array properties using data abstraction (NSAD 2020)

Sun 15 - Sat 21 November 2020 Online Conference

Who

Julien Braine, Laure Gonnord

Track

NSAD 2020

Time Zone

The program is currently displayed in (GMT-06:00) Central Time (US & Canada).

Use conference time zone: (GMT-06:00) Central Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 17 Nov 2020 03:40 - 04:00 at SPLASH-IV - Papers Chair(s): Liqian Chen, Khalil Ghorbal

Abstract

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.

Julien Braine

Laure Gonnord

University of Lyon & LIP, France

France