SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Wed 7 Dec 2022 16:30 - 17:00 at Lecture Theatre 2 - SAS Papers 2 Chair(s): Benoît Montagu

Shape analyses aim at inferring semantic invariants related to the data-structures that programs manipulate. To achieve that, they typically abstract the set of reachable states. By contrast, abstractions for transformation relations between input states and output states not only provide a finer description of program executions but also enable the composition of the effect of program fragments so as to make the analysis modular. However, few logics can efficiently capture such transformation relations. In this paper, we propose to use connectors inspired by separation logic to describe memory state transformations and to represent procedure summaries. Based on this abstraction, we design a top-down interprocedural analysis using shape transformation relations as procedure summaries. Finally, we report on implementation and evaluation.

Wed 7 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
15:30
30m
Talk
Compositional Verification of Smart Contracts Through Communication Abstraction
COVID Time Papers In Person
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Jorge A. Navas Certora, inc., Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys, Arie Gurfinkel University of Waterloo
Link to publication DOI
16:30
30m
Talk
Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries
COVID Time Papers In Person
Hugo Illous CEA & INRIA / ENS Paris, Matthieu Lemerre CEA LIST, France, Xavier Rival INRIA/CNRS/ENS Paris
Link to publication DOI