The paper proposes a new static analysis designed to handle open programs, i.e., fragments of programs, with dynamic pointer-linked data structures—in particular, various kinds of lists—that employ advanced low-level pointer operations. The goal is to allow such programs be analysed without a need of writing analysis harnesses that would first initialise the structures being handled. The approach builds on a special flavour of separation logic and the approach of biabduction. The code of interest is analyzed along the call tree, starting from its leaves, with each function analysed just once without any call context, leading to a set of contracts summarizing the behaviour of the analysed functions. In order to handle the considered programs, methods of abduction existing in the literature are significantly modified and extended in the paper. The proposed approach has been implemented in a tool prototype and successfully evaluated on not large but very complex programs.
Fri 10 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | Program Analysis 2Research Papers / Hub Talks at Aurora Borealis 1 Chair(s): Quentin Stiévenart Vrije Universiteit Brussel | ||
13:30 20mTalk | Low-Level Bi-AbductionECOOP 2022 Research Papers Lukáš Holík Brno University of Technology, Petr Peringer Brno University of Technology, Adam Rogalewicz Brno University of Technology, Faculty of Information Technology, Veronika Šoková Brno University of Technology, Tomáš Vojnar Brno University of Technology, Florian Zuleger TU Vienna | ||
13:50 20mTalk | On the computation of interprocedural weak control closureHub Talk Hub Talks Abu Naser Masud Malardalen University Link to publication DOI | ||
14:10 20mTalk | Slicing of Probabilistic Programs based on SpecificationsECOOP 2022 Research Papers Federico Olmedo University of Chile & IMFD Chile Pre-print | ||
14:30 20mTalk | A Deterministic Memory Allocator for Dynamic Symbolic ExecutionVCOOP 2022ECOOP 2022 Research Papers Daniel Schemmel Imperial College London, Julian Büning RWTH Aachen University, Frank Busse Imperial College London, Martin Nowack Imperial College London, Cristian Cadar Imperial College London, UK |