Jul 21, 2017 Comments Off on Organizers
Organizers
- Bor-Yuh Evan Chang (University of Colorado Boulder, USA)
- Xavier Rival (CNRS, ENS and INRIA, France)
- Sukyoung Ryu (KAIST, Korea)
Jul 21, 2017 Comments Off on Organizers
Jul 21, 2017 Comments Off on Participants
Jul 21, 2017 Comments Off on Schedule
Note: checkout time is until 10:00
Jul 21, 2017 Comments Off on Overview
Static analysis aims at computing semantic properties of programs, so as to verify properties such as absence of runtime errors, functional correctness, termination, security, and more. Since these properties are generally undecidable, automatic program analysis tools usually need to be conservative so as to attempt to prove properties of interest. In that process, they need to reason about all components of the semantics of programs (numeric and symbolic computations, parallelism, etc). The notion of abstraction is central in static analysis: an abstraction defines a set of logical properties that a program analysis tool may use, their meaning, and the supporting algorithms. Numeric abstractions made remarkable progresses early in the development of static analysis. However, to reason about complex languages (be it C, Java, ML, or JavaScript), analysis tools also need to use a careful abstraction of the structures stored in memory.
Many kinds of memory abstractions have been introduced in the last thirty years. Initially, memory abstractions mainly consisted of pointer abstractions based on aliasing graphs or points-to relations. Such abstractions cannot cope precisely with data-structures of unbounded size, thus shape analysis techniques were introduced in the 1990s. Shape analysis techniques rely on more complex mathematical objects to describe unbounded memory graphs by summarizing inductive patterns [2]. In the last decade, a large number of novel techniques and applications for memory abstractions have emerged. In the same time, novel abstractions for array data-structure have been developed, and many of these are able to summarize array regions of static or dynamic size. More recently, object structures have become common in dynamic languages and several abstractions have been proposed, that can deal with unbounded structures indexed over unordered keys.
Even though the development of memory abstractions still seems to be lagging compared to, e.g., numeric abstraction, recent progresses seem to make this field more mature. Structure-specific abstractions have been developed and implemented for most common memory data-structures. For most kinds of data-structures, we can now choose among several abstractions that provide different levels of performance in terms of precision and cost. Moreover, client analyses have been identified, that utilize memory abstractions to infer other kinds of properties (safety of sequential or parallel programs, termination, resource consumption…).
Still, the memory abstraction research field has several open questions such as:
The purpose of the meeting is to bring together experts in the design and in the use of memory abstractions, so as to leverage on the recent advances in this field, allow for the development of new fundamental principles and tools, and ease the use of memory abstractions in emerging applications. In the next two sections we elaborate on the two main aspects of the envisioned seminar, namely the memory abstraction techniques, and their applications. For each aspect, we explain why we think such a meeting would be timely, and outline the expected benefits.