6th International Workshop on Aliasing, Capabilities and Ownership (IWACO)

July 29th, 2014

 

Reasoning about shared state in imperative programs is challenging. The existence of aliases, in particular, compromises modular reasoning, making imperative programs hard to understand, maintain, and analyze. These difficulties become even aggravated in a concurrent context. On the other hand, aliasing is a very powerful feature and allows for efficient implementations of data structures, for example.

To address those challenges, techniques have been introduced for describing and reasoning about stateful programs and for restricting, analyzing, and preventing aliases. Approaches are based on ownership, capabilities, separation logic, linear logic, uniqueness, sharing control, escape analysis, argument independence, read-only references, linear references, effects systems, and access control mechanisms.

The workshop will generally address the question how to reason about stateful (sequential or concurrent) programs. In particular, we will consider the following issues (among others):

models, type and other formal systems, programming language mechanisms, analysis and design techniques, patterns and notations for expressing ownership, aliasing, capabilities, uniqueness, and related topics; optimization techniques, analysis algorithms, libraries, applications, and novel approaches exploiting ownership, aliasing, capabilities, uniqueness, and related topics; empirical studies of programs or experience reports from programming systems designed with these issues in mind; programming logics that deal with aliasing and/or shared state, or use ownership, capabilities or resourcing; applications of any of these techniques to a concurrent setting.

We encourage not only submissions presenting original research results, but also papers that attempt to establish links between different approaches and/or papers that include survey material. Original research results should be clearly described. Paper selection will be based on the quality of the submitted material. Please direct any questions regarding the workshop's scope to the workshop organizers.

Submissions page: https://www.easychair.org/conferences/?conf=iwaco2014

Link to CFP.

List of accepted papers.

Wokshop program.

Important Dates (new dates!)

Abstract submission: May 17, 2014

Paper submission: May 19, 2014

Notification: June 21, 2014

Final version: July 5, 2014

Workshop: July 29, 2014

All deadlines 23:59 AOE time.

Program Committee

Werner Dietl, University of Waterloo

Colin Gordon, University of Washington

Ana Milanova, Rensselaer Polytechnic Institute

Greg Morrisett, Harvard University

Frank Pfenning, Carnegie Mellon University

Francois Pottier, INRIA

Alex Summers, ETH Zürich

Aaron Turon, Max Planck Institute for Software Systems

Jan Vitek, Purdue University

Janina Voigt, Cambridge University

Organizers

Stephanie Balzer, Carnegie Mellon University

Johan Östlund, Uppsala University

Invited Speaker

Nicholas Cameron, senior research engineer, Mozilla Research.

Memory Safety without Garbage Collection - aliasing, regions, uniqueness, and immutability in Rust

========================================================================================

Systems programming requires unfettered access to memory and predictable, low-cost abstractions. As such, garbage collection is impractical. However, years of experience have shown that programming in a memory unsafe language (such as C or C++) results in subtle and hard to find bugs, often with severe implications for security. Rust solves these constraints using static type checking. Rust's type system tracks aliasing and prevents memory leaks, dangling pointers, use-after-free errors, data races, and other sources of memory unsafety, all without run-time overhead.

In this talk, I will give a brief overview of Rust's syntax and semantics; describe Rust's system of alias control - borrowed references, explicit lifetimes, unique pointers - and its implementation; show how these features conspire to ensure memory safety, including in a multi-threaded environment; show how uniqueness and mutability are coordinated to prevent data races and make programs easier to reason about; and show how the type system can be safely circumvented using dynamic checking, where necessary.

Steering Committee

Dave Clarke, Uppsala University

Sophia Drossopoulou, Imperial College

Peter Müller, ETH Zürich

James Noble, Victoria University of Wellington

Matthew Parkinson, Microsoft Research

Tobias Wrigstad, Uppsala University

Selection Process

Both full papers (up to 15 pages) and short papers (up to 8 pages) in LNCS format are welcome. All submissions will be reviewed by the program committee. The accepted papers, after rework by the authors, will be made publicly available as informal proceedings on the workshop web page.