No.108 Memory Abstraction, Emerging Techniques and Applications

• Bor-Yuh Evan Chang (University of Colorado Boulder, USA)
• Xavier Rival (CNRS, ENS and INRIA, France)
• Sukyoung Ryu (KAIST, Korea)

• Bor-Yuh Evan Chang (organizer)
• Patrick Cousot
• Arlen Cox
• Julian Dolby
• Cezara Drăgoi
• Philippa Gardner
• Nathan Keynes
• Yoonseok Ko
• Huisong Li
• Jiangchao Liu
• Anders Moeller
• Hakjoo Oh
• Jihyeok Park
• Xavier Rival (organizer)
• Sukyoung Ryu (organizer)
• Manuel Serrano
• Yannis Smaragdakis
• Caterina Urban
• Thomáš Vojnar
• Kwangkeun Yi
• Florian Zuleger

10th September (Sunday)

• 15:00 – 19:00 – Hotel Check In (early check-in from 12:00 is negotiable if informed in advance)
• 19:00 – 21:00 – Welcome Reception

11th September (Monday)

• 7:30 – 9:00 – Breakfast (Cafeteria “Oak”)
• 9:00 – 9:10 – Introduction Movie of NII Shonan Meetings
• 9:10 – 9:45 – Seminar introduction, and presentation of the members
• 9:45 – 10:30 – Talk: Arlen Cox
• 10:30 – 11:00 – Break
• 11:00 – 12:00 – Talks: Anders Møller / Manuel Serrano
• 12:00 – 13:30 – Lunch (Cafeteria “Oak”)
• 13:30 – 14:00 – Shooting of the group photo
• 14:00 – 15:30 – Talks: Xavier Rival / Yannis Smaragdakis
• 15:30 – 16:00 – Break
• 16:00 – 18:00 – Talks: Florian Zuleger / Jihyeok Park / Sukyoung Ryu / Bor-Yuh Evan Chang
• 18:00 – 19:30 – Dinner (Cafeteria “Oak”)

12th September (Tuesday)

• 7:30 – 9:00 Breakfast (Cafeteria “Oak”)
• 9:00 – 10:30 Talks: Kwangkeun Yi / Nathan Keynes
• 10:30 – 11:00 Break
• 11:00 – 12:00 Talks: Yoonseok Ko / Jiangchao Liu
• 12:00 – 13:30 Lunch (Cafeteria “Oak”)
• 13:30 – 15:00 Talks: Thomáš Vojnar / Julian Dolby
• 15:00 – 15:30 Break
• 15:30 – 17:15 Talks: Caterina Urban / Hakjoo Oh / Cezara Drăgoi
• 17:15 – 18:00 Discussion: Plan for the Week
• 18:00 – 19:30 Dinner (Cafeteria “Oak”)

13th September (Wednesday)

• 7:30 – 9:00 Breakfast (Cafeteria “Oak”)
• 9:00 – 10:30 Talks
• 10:30 – 11:00 Break
• 11:00 – 12:00 Talks
• 12:00 – 13:30 Lunch (Cafeteria “Oak”)
• 13:30 – 18:15 Excursion
• 18:15 – 19:30 Main Banquet

14th September (Thursday)

Note: checkout time is until 10:00

• 7:30 – 9:00 Breakfast (Cafeteria “Oak”)
• 9:00 – 10:30 Talks
• 10:30 – 11:00 Break
• 11:00 – 12:00 Talks
• 12:00 – 13:30 Lunch (Cafeteria “Oak”)
• 13:30 End of the Seminar

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 standardization of the concrete semantic models of programming languages regarding to memory;
• the unification of APIs between abstract domains;
• the scalability of summarizing abstractions;
• the cooperation between memory abstractions;
• the effective design of abstractions for data-structures found in dynamic languages;
• the emerging applications, e.g., to liveness, and security.

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.