Talks

(slides)

Ole Agesen

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.

PLDI
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.

(slides)

Amer Diwan

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.

PLDI
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.

Tobias Wrigstad

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.

ECOOP
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.

Greg Morrisett

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.

ECOOP
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.

Gernot Heiser

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.

LCTES
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.

Gavin Bierman & Claudio Russo

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).

ECOOP
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.

Tom Van Cutsem

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.

ECOOP
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).

Ole Lehrmann Madsen

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.

ECOOP
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.

John Regehr

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.

PLDI
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.

James Noble

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.

PLDI
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.

Jaejin Lee

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.
http://aces.snu.ac.kr/~jlee/Jaejin_Lees_Home/PLDI12_tutorial.html

PLDI
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.

Luca Mottola

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.
http://www.sics.se/~luca/pldiTutorial.pdf

PLDI
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.

Aditya Nori & Sriram Rajamani

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.
http://research.microsoft.com/en-us/projects/yogi/pldi2012.aspx

PLDI
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.

Armando Solar-Lezama

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.
PLDI
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.

David P. Grove

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.

ICOOOLPS
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.

Tom Van Cutsem

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.

FTfJP
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).

Anders Møller

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.

SOAP
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.

Gilles Barthe

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.

PLAS
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.

Dawn Song

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.

SSP
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.