SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Sun 17 Oct 2021 14:30 - 14:45 at Zurich B - Session 3A Chair(s): Mihaela Sighireanu
Sun 17 Oct 2021 22:30 - 22:45 at Zurich B - Session 3A Chair(s): Suvam Mukherjee

Proving properties on programs operating over arrays, or array-like data structures, most often involves universally quantified invariants, e.g., “all elements below index i are nonzero”. In this article, we propose a general data abstraction scheme operating on Horn Formula for which we provide a relative completeness resolution scheme: the generated purely scalar invariant search problem has a solution if and only if the original problem has one expressible by the abstraction.

Sun 17 Oct

Displayed time zone: Central Time (US & Canada) change

13:50 - 15:10
Session 3ASAS at Zurich B +8h
Chair(s): Mihaela Sighireanu IRIF, Université Paris Diderot, France
13:50
15m
Talk
Static Analysis of Endian Portability by Abstract InterpretationVirtual
SAS
David Delmas Airbus & Sorbonne Université, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
14:05
15m
Talk
Verified Functional Programming of an Abstract InterpreterVirtual
SAS
Lucas Franceschino INRIA, David Pichardie Facebook Paris, Jean-Pierre Talpin INRIA, France
14:30
15m
Talk
Data Abstraction: A General Framework to Handle Program Verification of Data StructuresVirtual
SAS
Julien Braine , Laure Gonnord University of Lyon & LIP, France, David Monniaux CNRS/VERIMAG
14:45
25m
Live Q&A
Session 3A Discussion, Questions and AnswersVirtual
SAS