SAS 2023
Sun 22 - Tue 24 October 2023 Cascais, Portugal
co-located with SPLASH 2023
Sun 22 Oct 2023 10:05 - 10:35 at Room I - Session 1 Chair(s): Caterina Urban

Traditional separation logic-based shape analyses utilize inductive summarizing predicates so as to capture general properties of the layout of data-structures, to verify accurate manipulations of, e.g., various forms of lists or trees. However, they also usually abstract away content properties, so that they may only verify memory safety and invariance of data-structure shapes. In this paper, we introduce a novel abstract domain to describe sequences of values of unbounded size, and track constraints on their length and on extremal values contained in them. We define a reduced product of such a sequence abstraction together with an existing shape abstraction so as to infer both shape and content properties of data-structures. We report on the implementation of the sequence domain, its integration into a static analyzer for C code, and we evaluate its ability to verify partial functional correctness properties for list and tree algorithms.

Sun 22 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Session 1SAS 2023 at Room I
Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL
SAS 2023
Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, José Morales IMDEA Software Institute
Goal-Directed Abstract Interpretation and Event-Driven FrameworksKeynote
SAS 2023
I: Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon
A Product of Shape and Sequence Abstractions (Radhia Cousot Young Researcher Best Paper Award)
SAS 2023
Josselin Giet Ecole Normale Supérieure, Félix Ridoux Univ Rennes / IMDEA Software Institute, Xavier Rival Inria; ENS; CNRS; PSL University