PLDI Keynotes

Heed the Rise of the Virtual Machines


Ole Agesen

Ole Agesen'ss picture

Virtual Machines have become ubiquitous; they now run about half of the world's x86 server workloads. For software developers as well as language designers and implementors, virtualization is a factor that should not be ignored. This talk looks inside a modern hypervisor to provide a qualitative understanding of how virtualization affects "guest" software. We aim to give the audience a basis for understanding and improving the performance of virtualized software.

Time: 8:45–9:45, June 11
Room: Ballroom A

Ole Agesen is Fellow at VMware where he has worked on virtualization technologies for over a decade. Before that he worked on the ExactVM at Sun labs, and on the Self programming language for his PhD at Stanford.

Parallelism From the Middle Out


Doug Lea

Doug Lea's picture

The range of users and range of applications of concurrency and parallelism support based on libraries and frameworks has shown steady evolutionary growth over the past decade. This talk presents some observations on library design, engineering, and usage, and their impact on the development of languages, VMs and runtime systems, platforms, and applications.

Time: 9:00–10:00, June 12
Room: Ballroom A

Doug Lea is a professor of computer science at State University of New York at Oswego where he specialises in concurrent programming and the design of concurrent data structures. He wrote "Concurrent Programming in Java: Design Principles and Patterns", one of the first books on the subject, and chaired JSR 166, which added concurrency utilities to Java.

Should You Trust Your Experimental Results?


Amer Diwan

Amer Diwan's picture

Experimentation is central to science, influencing all stages of scientific investigations. At the beginning of an investigation, we conduct experiments to understand a system’s nature, perhaps to identify performance bottlenecks or other weaknesses. Later on, we conduct experiments to evaluate innovations to the system or to test hypotheses. An improperly designed experiment can produce misleading results. Unfortunately, even with our best diligence, we may make a mistake and end up with an improperly-designed experiment. This talk will describe and illustrate a framework for reasoning about and recognizing many common errors in experimental design.

Time: 8:45–9:45, June 13
Room: Ballroom A

Amer Diwan is an engineer at Google focusing on the performance of Google services, particularly Gmail. Before Google, Amer was a professor at the University of Colorado at Boulder. His research interests include performance analysis, program analysis, and programmer productivity tools.

ECOOP Keynotes

Dahl Nygaard Junior Award: Structured Aliasing

Tobias Wrigstad

Tobias Wrigstad's picture

Aliasing, mutable state and stable object identities are inherent in object-oriented programming. It is a well-known fact that this troika of features cause problems for practitioners, tool developers and formalists alike. Patterns for aliasing, and patterns for structuring object graphs exist, and manipulating aliases and managing these graphs or graph-like structures are among the most frequent operations in object-oriented programming. Yet, mainstream languages provide only low-level support for these operations in reading and writing of variables. I will talk about my work on managing aliases in object-oriented systems, and talk about some recent efforts to unify these approaches to provide what we could call a theory and practise of structured aliasing.

Time:  8:45–10:00, June 14
Room:  Ballroom A

Tobias Wrigstad is an assistant professor at Uppsala University. He holds a PhD from The Royal Institute of Technology, Stockholm. After a types-heavy PhD, he went untyped in developing the scripting language Thorn in a joint project with Purdue and IBM. Tobias' most active research interests are object-oriented aliasing, parallel programming languages, and scripting languages.

When Compilers are Mirrors

Martin Odersky

Martin Odersky's picture

When compilers are reflective mirrors, interesting things happen. Reflection and compilers do tantalizing similar things. Yet, in mainstream, statically typed languages the two have been only loosely coupled, and generally share very little code. In this talk I explore what happens if one sets out to overcome their separation. The first half of the talk addresses the challenge how reflection libraries can share core data structures and algorithms with the language's compiler without having compiler internals leaking into the standard library API. The second half of the talk explores what one can do when strong, mirror-based reflection is a standard tool. In particular, the compiler itself can use reflection, leading to a particular system of low-level macros that rewrite syntax trees.

Time: 9:00–10:00, June 15
Room: Ballroom A

Martin Odersky is the inventor of the Scala language, a professor at EPFL, and a founder of Typesafe, Inc. His work concentrates on the fusion of functional and object-oriented programming. He has also influenced the development of Java as a co-designer of Java generics and the javac reference compiler.

ECOOP Banquet Speaker: The Harvard RoboBee Project

Greg Morrisett

Greg Morrisett's picture

Honey bees are responsible for pollinating about one third of the crops grown in the US. But for the past few years, bees have been disappearing at an alarming rate, due to a mysterious syndrome known as colony collapse disorder. The goal of our NSF-funded expedition is, ostensibly, to build an artificial swarm of insect-scale robots that can autonomously pollinate crops. The real goal is to push advances in miniature robotics and the design of compact high-energy power sources; spur innovations in ultra-low-power computing and electronic "smart" sensors; and refine coordination algorithms to manage multiple, independent machines.

Time:  19:00–21:30, June 15
Room:  ECOOP Banquet

Greg Morrisett received his Ph.D. from Carnegie Mellon in 1995, and in 1996, he took a faculty position at Cornell University. In 2004, he moved to Harvard as the Allen B. Cutting Professor of Computer Science, and served in the position of Associate Dean for Computer Science and Engineering from 2007-2010.

Morrisett served as Chief Editor for JFP and as an associate editor for ACM TOPLAS and IPL. He currently serves as an editor for JACM and as co-editor in chief for ACM CACM Research Highlights. Morrisett has also served on DARPA ISAT, the NSF CISE Advisory Council, Microsoft Research's Technical Advisory Board, and Microsoft's Trustworthy Computing Academic Advisory Board.

He has received a number of awards for his research on programming languages, type systems, and software security, including a Presidential Early Career Award, an IBM Faculty Fellowship, an NSF Career Award, and an Alfred P. Sloan Fellowship.

Having said all of this, he knows relatively little about bees or robots, and you should take everything he says with a large grain of salt.

LCTES Keynotes

Towards Trustworthy Embedded Systems

Gernot Heiser

Gernot Heiser's picture

Embedded systems are increasingly used in circumstances where people's lives or valuable assets are at stake, hence they should be trustworthy — safe, secure, reliable. True trustworthiness can only be achieved through mathematical proof of the relevant properties. Yet, real-world software systems are far too complex to make their formal verification tractable in the foreseeable future. The Trustworthy Systems project at NICTA has formally proved the functional correctness as well as other security-relevant properties of the seL4 microkernel. This talk will provide an overview of the principles underlying seL4, and the approach taken in its design, implementation and formal verification. It will also discuss on-going activities and our strategy for achieving the ultimate goal of system-wide security guarantees.

Time: 8:00–9:00, June 12
Room: Meeting 1

Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at the University of New South Wales (UNSW), and leads the Software Systems Research Group at NICTA, Australia's National Centre of Excellence for ICT Research. Gernot founded Open Kernel Labs, now the market leader in secure virtualization technology for embedded systems. The company's OKL4 operating system is deployed in more than 1.5 billion mobile devices.

Synchronous languages and their compilation

Nicolas Halbwachs

Nicolas's picture

During the last decades, synchronous programming has been a successful paradigm for designing critical embedded software. It gave rise to an increasing family of languages, and to industrial tools, like Scade (Esterel-Technologies) or RT-Builder (Geensoft), which are now commonly used in many domains (avionics, railways, energy,...) all over the world. In this talk, we shall recall the underlying principles of synchronous programming, and illustrate both imperative and data-flow synchronous styles. Then we shall present a survey of code generation techniques: the translation of imperative programs into data-flow; the generation of sequential code from data-flow programs; the generation of multi-task deterministic code, and several proposals for generating distributed code.

Time: 9:00–10:00, June 13
Room: Meeting 1

Nicolas Halbwachs is the Director of the Verimag Laboratory in Gernoble and is best known for his groundbreaking work on abstract interpretation and synchronous languages.

ISMM Keynote

Why Is Your Web Browser Using So Much Memory?

Robert O'Callahan

Robert O'Callahan's picture

Browsers are the operating systems of the Web. They support a vast universe of applications written in a modern garbage-collected programming language. Browsers expose a rich platform API mostly implemented in C++. Browsers are also consumer software with low switching costs in an intensely competitive market. Thus in addition to standard requirements such as maximizing throughput and minimizing latency, browsers have to consider issues like "when the user closes a window while watching Task Manager, they want to see memory usage go down". Browsers have to compete to minimize memory usage even for poorly written applications. In this talk I will elucidate these requirements and describe how Firefox and other browsers address them. I will pay particular attention to issues that we don't know how to solve, and that could benefit from research attention.

Time: 9:00–10:00, June 15
Room: Meeting 1

Robert O'Callahan obtained a PhD in programming languages and software engineering tools from CMU. After a few years at IBM Research working on dynamic program analysis, he returned to New Zealand to work on Mozilla full-time. Now he manages a growing team of Gecko developers in Auckland while still trying to write lots of code.

ECOOP Summer School

Controlling Mutation & Aliases with Fractional Permissions

John Boyland

John Boyland's picture
Mutation and aliases are a hallmark of imperative concurrent programming but can lead to confusion and to hard-to-detect and hard-to-repat race conditions. Fractional permissions allow one to specify mutation and aliasing restrictions using both simple flow-insensitive and complex flow-sensitive reasoning. The talk introduces fractional permissions with practical motivation and then shows how they can be used to encode concepts such as uniqueness, ownership and effects. Then discussion will move into larger concepts such as object invariants, mutation control in iterators, synchronization and reasoning with Java's volatiles. The last part of the talk will open the floor for a general discussion on other mutation patterns to see how fractional permissions can be applied in new ways.

Time: 10:30–12:00, June 15
Room: Conference 8

John Boyland is an Associate Professor at the University of Wisconsin-Milwaukee. He does research in the verification of aliasing restrictions and in proof systems. He received his doctorate under the direction of Susan Graham at Berkeley in 1996 in the area of attribute grammars. He was a post-doctoral fellow at Carnegie Mellon.

C# formally

Gavin Bierman & Claudio Russo

Gavin Bierman's pictureClaudio Russo's picture

C# is a modern, type-safe, OO language, designed for the Microsoft .NET platform. It has grown in popularity and is now in use by millions of developers around the world. But what sort of language is it? We prefer a precise, formal, mathematical answer. In this tutorial, we will show that C# can be given a formal description using familiar tools from the PL community: including subtyping by coercions, and type-directed and syntactic translations. We will show you how a middleweight core fragment can be formalized, and then how various C# extensions can be captured accurately; including LINQ (C# 3.0), dynamic (C# 4.0) and asynchronous programming (C# 5.0).

Time: 13:30–15:00, June 15
Room: Conference 8

Gavin Bierman is a senior researcher in the Programming Principles and Tools Group at Microsoft Research in Cambridge, UK. Prior to joining MSR, he was a faculty member at the University of Cambridge. He has a PhD from the University of Cambridge and a BSc from Imperial College, London. His interests include programming languages, database systems and big data.

Claudio Russo is a researcher in the Programming Principles and Tools Group at Microsoft Research in Cambridge, UK. He has a PhD and BSc from the University of Edinburgh and has worked on .NET generics, type systems for functional and object-oriented languages and concurrency abstractions.

Maxine: A Virtual Machine For, and In, Java

Christian Wimmer & Laurent Daynès

Christian Wimmer's pictureLaurent Daynes's picture

Writing a VM in Java makes it more approachable. VM implementation is facilitated by the palette of features supported by Java, most notably type and memory safety, garbage collection, exception handling, reflection, and annotations. The Maxine VM is a meta-circular VM implementation that aggressively uses these features. It is co-designed with a custom debugging companion tool, the Maxine VM Inspector, that combines inspection of a running VM image with debugging features. We believe that this approach makes Maxine one of the most approachable VMs, and therefore a good basis for academic research and teaching. Graal is the optimizing JIT that originated from the JIT compiler in Maxine, but is now a self-contained OpenJDK project and also integrated in HotSpot. We will present the architecture and design decisions behind Maxine and Graal, and give an introduction to the source code so that researchers can get started writing their own extensions and optimizations.

Time: 15:30–17:00, June 15
Room: Conference 8

Christian Wimmer is a researcher at Oracle Labs, working on the Maxine VM, on the Graal compiler project, as well as on other projects that involve dynamic compilation and optimizations. His research interests span from compilers, virtual machines, and secure systems to component-based software architectures.

Laurent Daynès is a member of the Maxine project at Oracle Labs. He is working on garbage collection and meta-circular implementation of virtual machine for modern programming languages. Prior to joining the Maxine project, he worked in the Barcelona project where he was the main contributor to MVM, the multi-tasking virtual machine.

Javascript's Meta-Object Protocol

Tom Van Cutsem

Tom Van Cutsem's picture

In this talk, we will give a fast-paced tutorial on the Javascript programming language. Subsequently, we introduce a new reflection API that will be added in the next standard edition of Javascript. This API enables Javascript programmers to create proxies, which are essentially objects with a customizable meta-object protocol. Proxies are a cornerstone technology enabling among others transparent sandboxing of applications, virtualizing browser APIs and language extensions such as higher-order contracts. By mastering this API, you will gain a better insight into the true nature of Javascript's object model.

Time: 8:30–10:00, June 16
Room: Conference 8

Tom Van Cutsem is a researcher at the Vrije Universiteit Brussel, Belgium. He finished his PhD in 2008 on the topic of AmbientTalk, a distributed object-oriented scripting language for mobile phones. Since 2010, he serves on the ECMAScript standardization committee, where he designed the Javascript Proxy API in close collaboration with Mark S. Miller (Google).

Abstract Reasoning about Concurrent Modules

Philippa Gardner

Philippa Gardner's picture

Reasoning about concurrent programs has long been recognised as challenging. Whereas programmers understand how to think modularly about programs, the reasoning has not matched this modular thinking. Abstraction is the key to modular reasoning. I will describe recent work on program logics for reasoning abstractly about concurrent modules. This work is part of a stream of work on local reasoning about concurrent programs, initiated by the work on concurrent separation logic. Concurrent separation logic provides course-grained reasoning about concurrent modules, for example reasoning about a whole set. RGSep and deny-guarantee reasoning provides fine-grained reasoning about, for example, elements of the linked list, but cannot abstract to fine-grained reasoning about elements of a set. I will describe recent work on fine-grained abstract reasoning about concurrent modules, using recent work by myself and others on concurrent abstract predicates and views.

Time: 10:30–12:00, June 16
Room: Conference 8

Philippa Gardner is a Professor at Imperial College London. Her work unifies a range of research areas, including program verification, logic, concurrency, databases and the Web. She previously held a Microsoft/Royal Academy of Engineering Senior Research Fellowship at Imperial at Cambridge working on process models with Robin Milner. She completed a PhD on type theory and logical frameworks at Edinburgh, supervised by Gordon Plotkin.

The Scandinavian Approach

Ole Lehrmann Madsen

Ole Lehrmann Madsen's picture

SIMULA, the first OO language, was originally motivated by problems in operational research and simulation. The aim of providing a language for modeling as well as programming was also a major goal in the design of BETA. In BETA, language mechanisms such as class and method were unified into the pattern mechanism; the notion of virtual pattern (class) was introduced just as BETA further developed the SIMULA notion of quasi-parallel systems into full concurrency. In addition, a conceptual framework for proving a basis for OO modeling was developed. Current mainstream languages for modeling and programming are diverging. On one hand developers who would like to apply OO design to obtain a suitable model end up with the challenge of maintaining both model and program artifacts. And, since many modeling languages are at the same level of abstraction as programming languages, there is little benefit to using a separate modeling language. On the other hand we see that developers write a considerable amount of code with little appreciation of design and development disciplines. In the talk I describe the Scandinavian approach to OO, including lessons from SIMULA and BETA, the approach to object-oriented modeling, the associated conceptual framework, as well as problems and issues related to OO modeling and programming.

Time: 13:00–15:00, June 16
Room: Conference 8

Ole Lehrmann Madsen is a Professor of Computer Science at Aarhus University, and managing director of the Alexandra Institute Ltd. — a non-profit company doing application-oriented research within ICT in partnership with universities, companies and public institutions. He has worked with object-technology for more than 25 years starting with Simula programming. He developed the BETA programming language together with Kristen Nygaard, Birger Møller-Pedersen and Bent Bruun Kristensen.

PLDI Tutorials

Hardening Tools for C

John Regehr

John Regehr's picture

The target audience for this tutorial is interested in increasing the quality of one or more tools that process C code. Csmith, our random program generator, is useful in this regard, having uncovered more than 400 previously unknown bugs in C compilers and more than 50 bugs in non-compiler tools (such as static analyzers) for C. The focus will be on pragmatic issues such as choosing appropriate invariants to test, selecting an appropriate C subset, narrowing down the circumstances leading to tool failure, and automating the testing workflow.

Time: 11:00–12:30, June 12
Room: Conference 8

John Regehr is an associate professor in computer science at the University of Utah. His research focuses on improving software quality.

McLab, a Compiler and VM Framework for MATLAB

Laurie Hendren

Laurie Hendren's picture

MATLAB is a popular dynamic programming language used for scientific and numerical programming. As a language, it has evolved from a small scripting language intended as an interactive interface to numerical libraries, to a very popular language supporting many language features and libraries. The overloaded syntax and dynamic nature of the language, plus the somewhat organic addition of language features over the years, makes static analysis of modern MATLAB quite challenging. The tutorial will introduce the MATLAB language, the importance of compiler research for MATLAB and similar dynamic scientific languages, and the particular challenges the language presents for compiler developers. The tutorial will then provide an overview of the McLAB infrastructure, with a more in-depth presentation of the static analysis framework.

Time: 13:30–15:00, June 12
Room: Conference 8

Laurie Hendren leads the Sable Research Group. She has been a professor at McGill since 1990, was made an ACM Fellow in 2010, and was awarded a Canada Research Chair in Compiler Tools and Techniques in 2011. The Sable Research Group has previously designed and implemented Soot and associated tools for the analysis and transformation of Java.

Grace: an Open-Source OO Educational Programming Language

James Noble

James Noble's picture

Grace aims to demonstrate the advantages of object-orientation, showing how a small number of underlying principles can be applied uniformly: programs built from nested objects, computation as requesting behaviour from objects, and the separation of types and classes. Grace makes it possible to write powerful libraries that extend the language, supporting first-class pattern matching, parser combinators, and flexible control structures. Grace also supports, but does not require, static type checking. This makes it possible to use Grace as a dynamically typed language, to start with dynamic types and add static types later, or to teach static types from the beginning. In this talk, I'll outline the principal features of Grace, discuss open issues, and listen to your reactions while some choices are still on the table. I'll give some examples from the design process so far, showing how conceptually orthogonal design decisions all too easily end up as tightly coupled gordian knots.

Time: 10:45–12:15, June 13
Room: Conference 8

James Noble is a professor at Victoria University of Wellington, New Zealand. James's research centres around software design.

Data Parallel Programming in Haskell

Manuel Chakravarty

Manuel Chakravarty's picture

The Glasgow Haskell Compiler comes with support for a range of concurrent and parallel programming models, which take advantage of Haskell's rigorous control of side effects. In this talk, we will specifically focus on data parallel programming for shared-memory hardware, covering both regular and nested data parallelism as well as targeting both CPUs and GPUs. We will have a detailed look at how to write data parallel code in Haskell by discussing the implementation of example applications, such as edge detection and particle systems. This talk will give an overview over the state of the art of data parallel programming in Haskell. It will outline the range of use of the existing technology and show you how to get started on writing your own data parallel programs.

Time: 13:30–15:00, June 13
Room: Conference 8

Manuel Chakravarty is an Associate Professor at the University of New South Wales. He holds a doctoral degree from the Berlin Institute of Technology. He contributed to Haskell's foreign function interface, the theory and implementation of type families, and the design and realisation of Data Parallel Haskell, an implementation of nested data parallelism in the Glasgow Haskell Compiler.

SnuCL: An OpenCL Framework for Heterogeneous CPU+GPU Clusters

Jaejin Lee

Jaejin Lee's picture

Open Computing Language (OpenCL) is a programming model for heterogeneous parallel computing systems. OpenCL provides a common abstraction layer across different multicore architectures, such as CPUs, GPUs, DSPs, and Cell BE processors. Programmers can write an OpenCL application once and run it on any OpenCL-compliant system. However, current OpenCL is restricted to a single operating system instance. To target heterogenous CPU/GPU clusters, programmers must use the OpenCL framework combining with a communication library, such as MPI. This tutorial will cover usages and internals of an OpenCL framework, called SnuCL. It naturally extends the original OpenCL semantics to the heterogeneous cluster environment. The target cluster contains multiple CPUs and GPUs in a node. The nodes in the cluster are connected by an interconnection network, such as Gigabit and InfiniBand switches. For such clusters, SnuCL provides an illusion of a single operating system image for the programmer. With SnuCL, OpenCL applications written for a single operating system instance with multiple OpenCL compute devices can run on the cluster without any modification. This tutorial will introduce you to OpenCL and how OpenCL applications are developed for heterogeneous computing systems.

Time: 13:30–16:30, June 14
Room: Conference 9

Jaejin Lee is the director of the Center for Manycore Programming and a professor of Computer Science and Engineering at Seoul National University. He obtained a Ph.D. from UIUC in 1999 in the area of compilation techniques for explicitly parallel programs. His primary research focus in these days is on heterogeneous parallel programming models such as OpenCL.


Avik Chaudhuri

Avik Chaudhuri's picture

ActionScript is the programming language underlying Flash applications. It is a close cousin of JavaScript, and further includes classes and optional type annotations. An ActionScript program can be compiled to byte code and executed by a virtual machine embedded in the Flash player, so that it can run on desktop browsers. Alternatively, an ActionScript program can be compiled to machine code with the Flash integrated runtime, so that it can run natively on mobile platforms. In this tutorial, we begin by demonstrating how a sophisticated 3D first-person shooter game can be developed in ActionScript, relying on a combination of low-level Flash 3D APIs and high-level external 3D application frameworks. We then dive into the design and implementation of ActionScript itself. We discuss idiosyncrasies in the the current design of ActionScript, and related implementation challenges. We report experimental results that indicate that small "fixes" to the current semantics of the language can enable aggressive optimizations. Next, we outline early ongoing research on advanced language features for ActionScript. In particular, we sketch a type system with generics, that improves on related type systems in existing languages in terms of consistency, complexity, and soundness. We also sketch a STM-based system for concurrency control that offers a simpler atomicity semantics for transactions than existing systems in the midst of nesting and non-transactional code. Finally, we sketch a system for executing data-parallel programs adaptively on the CPU and the GPU. All of these advanced language features---generics, concurrency, parallelism---are motivated by the goal of improving the simplicity, correctness, and performance.

Time:9:00–12:00, June 15
Room: Conference 3

Avik Chaudhuri is a programming language design expert at Adobe Systems, where his overall role is to shape the future of the language in which Flash-based games are developed. Prior to joining Adobe, he completed a PhD at UCSC in 2008 and a post-doc at UMD in 2010.

Abstractions & Languages for Wireless Sensor Networks

Luca Mottola

Luca Mottola's picture

Wireless Sensor Networks (WSNs) are currently regarded as a key technology towards the vision of an “Internet of Things”. The current practice in programming WSNs largely revolves around low-level programming frameworks. Such an approach is not sustainable in the long term, and is certainly not applicable when WSNs become part of a larger computing infrastructure. In this tutorial, we begin with a characterization of WSN applications to identify the fundamental requirements at stake, and describe a taxonomy of high-level WSN programming solutions providing a foundation to classify, compare, and evaluate the various approaches. We intertwine the description with live demonstrations of the technology being discussed. The tutorial is aimed at fresh students looking for interesting problems, researchers willing to gain deeper insights into WSN programming, and practitioners in search of a systematic overview on the topic.

Time: 13:30–16:30, June 15
Room: Conference 3

Luca Mottola is an assistant professor at Politecnico di Milano and a Senior Researcher at the Swedish Institute of Computer Science. His research interests include the design, implementation, and validation of modern distributed systems, with the current focus on Internet of Things. He was listed amongst Postscapes "Internet of Things Top 100 Thinkers" and has received the Cor Baayen Award for the most promising young researcher in computer science and applied mathematics.

The K Framework

Grigore Rosu

Grigore Rosu's picture

K is an executable modular framework for programming language semantics, design and analysis. It is particularly suitable for defining truly concurrent languages/calculi, as well as for defining control-intensive language features such as abrupt termination, exceptions, or call/cc. K has been used to define real world languages like C. This tutorial will provide participants with a basic knowledge of the framework, showing how you can automatically generate an interpreter, debugger, state space searcher, and other formal analysis tools, all from an arbitrary language semantic definition using K. To exemplify the framework, prototypical languages covering the imperative, functional, object-oriented and logic programming paradigms will be defined.

Time: 9:00–12:00, June 16
Room: Conference 3

Grigore Rosu is an Associate Professor at the University of Illinois at Urbana-Champaign. His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering and programming languages. Before joining UIUC in 2002, he was a research scientist at NASA Ames.

Yogi: Property Checking via Static Analysis and Testing

Aditya Nori & Sriram Rajamani

Aditya V. Nori's pictureSriram K. Rajamani 's picture

Static analysis and testing are complementary approaches to the property checking problem. The goal of Yogi is to solve the property checking problem. One of the unique features of Yogi is that it simultaneously searches for both a test to establish that the program violates the property, and an abstraction to establish that the program satisfies the property. If the abstraction has a path that leads to the violation of the property, Yogi attempts to focus test case generation along that path. If such a test case cannot be generated, Yogi uses information from the unsatisfiable constraint from the test case generator to refine the abstraction. Thus, the construction of test cases and abstraction proceed hand-in-hand, using error traces in the abstraction to guide test case generation, and constraints from failed test-case generation attempts to guide refinement of the abstraction.

Time: 13:30–16:30, June 16
Room: Conference 9

Aditya V. Nori is a researcher at Microsoft Research India. His research interests include program analysis and machine learning with special focus on tools for improving software reliability and programmer productivity. He received his PhD from the Indian Institute of Science.

Sriram K. Rajamani is the assistant managing director of Microsoft Research India. His research interests are in programming languages and tools. Several of his projects have influenced academia and industry, the most notable one being SLAM which is the basis for Microsoft's Static Driver Verifier. He holds a PhD from the University of California at Berkeley.

Developing and Using Pluggable Type Systems

Werner Dietl

Werner M. Dietl's picture

A pluggable type system extends a language's built-in type system to confer additional compile-time guarantees. We will explain the theory and practice of pluggable types. The material is relevant for researchers who wish to apply type theory, and for anyone who wishes to increase confidence in their code. After this session, you will have the knowledge to: analyze a problem to determine whether pluggable type-checking is appropriate; design a domain-specific type system; implement a simple type-checker; scale a simple type-checker to more sophisticated properties; and better appreciate both object-oriented types and flexible verification techniques. While the theory is general, our hands-on exercises will use a state-of-the-art system, the Checker Framework, that works for the Java language, scales to millions of lines of code, and is being adopted in the research and industrial communities. Such a framework enables researchers to easily evaluate their type systems in the context of a widely-used industrial language, Java. It enables non-researchers to verify their code in a lightweight way and to create custom analyses. And it enables students to better appreciate type system concepts.

Time: 9:00–12:00, June 16
Room: Conference 9

Werner M. Dietl is a research associate at the Computer Science & Engineering department, University of Washington. He holds a PhD from ETH Zurich.

The Sketching Approach to Program Synthesis

Armando Solar-Lezama

Armando Solar-Lezama's picture

The Sketch synthesis system allows programmers to write complex routines while leaving fragments of the code unspecified; the contents of these "holes" in the program is derived automatically by a synthesis engine. Sketching allows programmers to focus the power of the synthesizer on those portions of the code that are menial but easy to get wrong, reducing programmer effort without overwhelming the synthesizer. This tutorial offers a hands-on introduction to sketching as implemented in the SKETCH language and its accompanying synthesizer and show how the synthesizer can be used to derive the low-level details in a complex algorithm from a sketch that expresses its high-level structure. Basic sketching techniques will be illustrated through examples involving manipulations of linked data-structures, low-level bit-manipulation algorithms such as ciphers and error correction codes, and stencil kernels from scientific computing.
Time: 13:30–16:30, June 16
Room: Conference 3

Armando Solar-Lezama is an assistant professor in the electrical engineering and computer science department at MIT. His research interests lay in the area of computer supported programming; in particular, he is interested in program synthesis and program analysis tools to support programmer productivity.

Workshop Keynotes

Implementing X10: Spanning High-Performance Computing & Big Data

David P. Grove

Dawn's picture

X10 is a modern object-oriented language that extends a Java-like core sequential language with closures, constrained types, and type inference. X10 also includes novel language features for fine-grained concurrency (finish, async, atomic) and distribution (Places, at). These features were originally motivated by the challenge of productively programming extremely large distributed memory supercomputers, but are equally applicable to emerging challenges in productively programming Big Data applications. X10 is implemented via source-to-source compilation to both C++ (Native X10) and Java (Managed X10). In this talk I'll discuss some of the key design decisions made in the X10 implementation, motivate why both Native X10 and Managed X10 are necessary, and discuss some of the challenges faced and insights gained in the process of implementing a full-fledged language using two fundamentally different substrates.

Time:; June 11
Room: Meeting 1

David P. Grove is a Research Staff Member in the Programming Technologies Department at the Watson Research Center. He also manages the Parallel Languages, Applications, and Tools group.

The Evolution of the JavaScript Engine

David Mandelin

Dave's picture

JavaScript was introduced in 1995 as a scripting language for the web, at first for little more than interactive menus and crude demos. JavaScript today is the scripting language, programming language, and even assembly language of the web. Now JavaScript is used to make beautiful 3D demos, games, and apps, and to run programs ported from languages such as C++. This talk is a history of JavaScript engine performance, especially the last five years, which I directly experienced. I'll talk about the different architectures and compilers implementers have tried, as engines evolved from simple interpreters to optimized interpreters and through multiple generations of JIT compilers. I'll also talk about the environment that shaped that evolution: the ideas, demos, and benchmarks that pushed and pulled implementers along. I'll conclude with some thoughts about things that haven't been tried yet, what users and the web need from JavaScript now, and where JavaScript engines might be headed next.

Time: 9:45–10:45, June 11
Room: NS

Dave Mandelin is manager of the JavaScript team at Mozilla and is also the module owner of the SpiderMonkey JavaScript engine. Previously, he was an engineer at Mozilla, working mainly on program analysis and then JavaScript performance. He is one of the author of trace-based Just-in-time compiler that was published at PLDI'09.

AmbientTalk: Modern Actors for Modern Networks

Tom Van Cutsem

Dawn's picture

We introduce AmbientTalk, a dynamic, object-oriented, distributed programming language.AmbientTalk focuses primarily on the domain of mobile peer-to-peer applications, which are becoming more and more widespread in the wake of smartphone platforms such as iOS and Android. AmbientTalk runs on Android, and can be thought of as a scripting language for that platform. We will discuss AmbientTalk~Rs roots and devote special attention to its concurrent and distributed language features, which are founded on the actor model. Next, we will showcase the language by explaining a peer-to-peer application. We show how resilient mobile applications can be constructed with familiar building blocks like objects and messages, but also in what way these building blocks have to be adapted to fit the characteristics of mobile networks.

Time: June 12
Room: Conference 9

Tom Van Cutsem is a researcher at the Vrije Universiteit Brussel, Belgium. He finished his PhD in 2008 on the topic of AmbientTalk, a distributed object-oriented scripting language for mobile phones. Since 2010, he serves on the ECMAScript standardization committee, where he designed the Javascript Proxy API in close collaboration with Mark S. Miller (Google).

Featherweight X10: a core calculus for async-finish parallelism

Jens Palsberg

Dawn's picture

We present a core calculus with two of X10's key constructs for parallelism, namely async and finish. Our calculus forms a convenient basis for type systems and static analyses for languages with async-finish parallelism. For example, we present a type system for context-sensitive may-happen-in-parallel analysis, along with experimental results of performing type inference on 13,000 lines of X10 code. Our analysis runs in polynomial time and produces a low number of false positives, which suggests that our analysis is a good basis for other analyses such as race detectors. Our calculus is also a good basis for tractable proofs of correctness. For example, we give a one-page proof of the deadlock-freedom theorem of Saraswat and Jagadeesan, and we prove the correctness of our type system.

Time:  June 12
Room:  Conference 9

Jens Palsberg is Professor and Chair of Computer Science at the University of California, Los Angeles. He is the editor-in-chief of ACM Transactions of Programming Languages and Systems and a member of the editorial board of Information and Computation.

Static Analysis for JavaScript vs. Java

Anders Møller

Anders Møller's picture

Dynamic languages such as JavaScript have become immensely popular, but programmers still rely on tedious testing to find even the simplest errors in their code. How can we build static analysis tools for JavaScript to help the programmers write better code? What makes JavaScript more challenging than Java, seen from a static analysis point of view? This talk gives an overview of lessons learned from two research projects - one involving string analysis for Java, and one about dataflow analysis for JavaScript.

Time: 9:00–10:00, June 14
Room: Conference 5

Anders Møller is associate professor at Aarhus University where he is manager of the Center for Advanced Software Analysis.

How languages can secure the future distributed environment

Andrew Myers

Myers's picture

The trend is clear: people are exchanging code and data increasingly freely across the Internet and the Web. But both code and data are vectors for attacks on confidentiality and integrity. The Fabric project is developing a new system to support the kinds of activities now happening on the Web: the free exchange of code and data across a decentralized, distributed system. Unlike the Web, Fabric has a principled basis for security: language-based information flow. By raising the level of abstraction for programmers, Fabric also makes it easier to reason clearly about security, even in the presence of distrusted mobile code. However, some interesting problems must be solved before a system like Fabric sees widespread adoption.

Time: June 15
Room: Conference 5

Andrew Myers Andrew Myers is a Professor at Cornell University. He is the recipient of an Alfred P. Sloan Research Fellowship, a George M. Sprowls award for outstanding MIT Ph.D. thesis, the Cornell Provost's Award for Distinguished Scholarship, the SIGPLAN Most Influential POPL Paper award for a paper in POPL 1999.

Computer-Aided Cryptographic Proofs

Gilles Barthe

Myers's picture

EasyCrypt is a toolset that assists the construction and verification of cryptographic proofs; it supports common patterns of reasoning in cryptography, and has been used successfully to prove the security of many examples, including encryption schemes, signature schemes, zero-knowledge protocols and hash functions. I will present recent developments in the tool and survey new applications.

Time: June 15
Room: Conference 5

Gilles Barthe works at the IMDEA Software Institute. Previously, he headed the Everest team on security at INRIA Sophia-Antipolis. He expertise is in formal methods, verification, security, cryptography, and foundations of mathematics and computer science.

Detecting Memory Leaks Statically Using Open64

Jingling Xue

Dusko's picture

Memory leaks are common errors affecting programs including OS kernels, desktop applications and web services. Many memory leaks result in serious software reliability problems. This talk will examine how to apply pointer analysis to detect memory leaks in C/C++ programs, by reviewing the state-of-the art techniques and presenting our recent work based on full-sparse value-flow analysis and implemented in Open64. I will discuss some promising results we achieved and some of the challenges we experienced

Time: 9:00–10:00, June 15
Room: Meeting 2

Jingling Xue is a Professor of Computer Science and Engineering at the University of New South Wales. He leads the Programming Languages and Compilers Group and its subgroup Compiler Research Group (CORG) at UNSW. His research interests are programming languages, compiler optimisations, computer architecture, parallel computing, distributed systems and cluster computing, and embedded systems.

Automatic Security Analysis in Binary, Web and Android

Dawn Song

Dawn's picture

In the BitBlaze project, we build a unified binary program analysis platform and use it for automatic vulnerability discovery and defense, in-depth malware analysis, and automatic extraction of security models for analysis and verification. The BitBlaze Binary Analysis Infrastructure is a fusion of static and dynamic analysis techniques and enables a set of powerful symbolic reasoning techniques on program binaries. I will also talk about BitTurner, the first public cloud-based service for automatic test case generation and security audit powered by dynamic symbolic execution on program binaries. I will give an overview of the WebBlaze project, aiming at designing and developing new techniques and tools to improve web security, including automatic dynamic symbolic execution on JavaScript for in-depth vulnerability detection in rich web applications. Finally, I will describe some ongoing efforts in DroidBlaze, an automatic security analysis infrastructure for Android apps.

Time: 9:00–10:00, June 16
Room: Conference 5

Dawn Song is an Associate Professor at Berkeley. She is the recipient of a MacArthur Fellowship, a Guggenheim Fellowship, a NSF CAREER Award, the Alfred P. Sloan Research Fellowship, the MIT Technology Review TR-35 Award, the IBM Faculty Award, the George Tallman Ladd Research Award and the Okawa Foundation Research Award.

Towards a theory of adaptive defense

Dusko Pavlovic

Dusko's picture

Modern cryptographic definitions of security usually go something like: "For all computationally feasible attack algorithms, the chance of success is negligible". On one hand, the restriction to feasible algorithms means that attacker's computational limitations are duly taken into account. This is, of course, the pivot point of modern cryptography, which is built upon the theory of computational complexity. On the other hand, though, the universal quantifier over all feasible algorithms implies that, if a feasible attack algorithm exists, the attacker is expected construct it soon enough. But there are, of course, feasible algorithms that are extremely hard to construct. So our attacker models have been refined to take attacker's computational limitations into account, but we still don't take into account his logical and programming limitations. We don't view the attacker as an omnipotent computer any more, like we did 40 years ago, but we still view him as an omnipotent programmer. This is, of course, not an unsafe view, just like the view that the attacker can compute whatever is computable wasn't unsafe. But maybe we are missing on a security resource, like we were missing on computational complexity. Can we take into account attackers' logical limitations, and use them like we use attackers' computational limitations? Is there a theory of logical complexity, that could play in algorithm protection the role that theory of computational complexity is nowadays playing in data protection?

Time: 14:00–15:00, June 16
Room: Conference 5

Dusko Pavlovic works at the Kestrel Institute.

Can Parallel Data Structures Rely on Automatic Memory Managers?

Erez Petrank

Dusko's picture

The complexity of parallel data structures is often measured by two major factors: the throughput they provide and the progress they guarantee. Concurrent access (and furthermore, optimistic access) to shared objects makes the management of memory one of the more complex aspects of concurrent algorithm design. The use of automatic memory management greatly simplifies the design of parallel algorithms. However, currently we do not know how to build a practical automatic memory manager that supports concurrent algorithms with progress guarantees. This talk examines the current state-of-the-art memory management support for concurrent algorithms, and spells out the most difficult open problem facing the memory management community today.

Time: June 16
Room: Meeting 1

Erez Petrank is a professor of computer science at the Technion. Erez's research interests are in the areas of memory management and parallel algorithms. He has been active in designing concurrent data structures and various memory management algorithms. He also participated in the construction of practical systems at IBM and at Microsoft.