Powered by

Conference Publishing Consulting

37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016), June 13–17, 2016, Santa Barbara, CA, USA

PLDI 2016 – Proceedings

Contents - Abstracts - Authors

Frontmatter

Message from the Chairs

Keynote Presentations

Sponsors and Supporters

Research Papers

Down to the Metal I

Into the Depths of C: Elaborating the De Facto Standards
Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK)

Living on the Edge: Rapid-Toggling Probes with Cross-Modification on x86
Buddhika Chamith, Bo Joel Svensson, Luke Dalessandro, and Ryan R. Newton
(Indiana University, USA)

Polymorphic Type Inference for Machine Code
Matt Noonan, Alexey Loginov, and David Cok
(GrammaTech, USA)

Verification I

Data-Driven Precondition Inference with Learned Features
Saswat Padhi, Rahul Sharma, and Todd Millstein
(University of California at Los Angeles, USA; Stanford University, USA)

Cartesian Hoare Logic for Verifying k-Safety Properties
Marcelo Sousa and Isil Dillig
(University of Oxford, UK; University of Texas at Austin, USA)

Verifying Bit-Manipulations of Floating-Point
Wonyeol Lee, Rahul Sharma, and Alex Aiken
(Stanford University, USA)

Testing and Debugging

Coverage-Directed Differential Testing of JVM Implementations
Yuting Chen, Ting Su, Chengnian Sun, Zhendong Su, and Jianjun Zhao
(Shanghai Jiao Tong University, China; East China Normal University, China; University of California at Davis, USA; Kyushu University, Japan)

Exposing Errors Related to Weak Memory in GPU Applications
Tyler Sorensen and Alastair F. Donaldson
(Imperial College London, UK)

Lightweight Computation Tree Tracing for Lazy Functional Languages
Maarten Faddegon and Olaf Chitil
(University of Kent, UK)

Energy and Performance

Effective Padding of Multidimensional Arrays to Avoid Cache Conflict Misses
Changwan Hong, Wenlei Bao, Albert Cohen, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, J. Ramanujam, and P. Sadayappan
(Ohio State University, USA; Inria, France; ENS, France; Pacific Northwest National Laboratory, USA; Louisiana State University, USA)

GreenWeb: Language Extensions for Energy-Efficient Mobile Web Computing
Yuhao Zhu and Vijay Janapa Reddi
(University of Texas at Austin, USA)

Input Responsiveness: Using Canary Inputs to Dynamically Steer Approximation
Michael A. Laurenzano, Parker Hill, Mehrzad Samadi, Scott Mahlke, Jason Mars, and Lingjia Tang
(University of Michigan, USA)

New Languages

Configuration Synthesis for Programmable Analog Devices with Arco
Sara Achour, Rahul Sarpeshkar, and Martin C. Rinard
(Massachusetts Institute of Technology, USA; Dartmouth College, USA)

From Datalog to Flix: A Declarative Language for Fixed Points on Lattices
Magnus Madsen, Ming-Ho Yee, and Ondřej Lhoták
(University of Waterloo, Canada)

Latte: A Language, Compiler, and Runtime for Elegant and Efficient Deep Neural Networks
Leonard Truong, Rajkishore Barik, Ehsan Totoni, Hai Liu, Chick Markley, Armando Fox, and Tatiana Shpeisman
(Intel Labs, USA; University of California at Berkeley, USA)

Parsing and Compilation

On the Complexity and Performance of Parsing with Derivatives
Michael D. Adams, Celeste Hollenbeck, and Matthew Might
(University of Utah, USA)

Down to the Metal II

Stratified Synthesis: Automatically Learning the x86-64 Instruction Set
Stefan Heule, Eric Schkufza, Rahul Sharma, and Alex Aiken
(Stanford University, USA; VMware, USA)

Remix: Online Detection and Repair of Cache Contention for the JVM
Ariel Eizenberg, Shiliang Hu, Gilles Pokam, and Joseph Devietti
(University of Pennsylvania, USA; Intel, USA)

Statistical Similarity of Binaries
Yaniv David, Nimrod Partush, and Eran Yahav
(Technion, Israel)

Types I

Accepting Blame for Safe Tunneled Exceptions
Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, and Andrew C. Myers
(Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA)

Occurrence Typing Modulo Theories
Andrew M. Kent, David Kempe, and Sam Tobin-Hochstadt
(Indiana University, USA)

Refinement Types for TypeScript
Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala
(University of California at San Diego, USA)

Synthesis I

MapReduce Program Synthesis
Calvin Smith and Aws Albarghouthi
(University of Wisconsin-Madison, USA)

Programmatic and Direct Manipulation, Together at Last
Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers
(University of Chicago, USA)

Fast Synthesis of Fast Collections
Calvin Loncaric, Emina Torlak, and Michael D. Ernst
(University of Washington, USA)

Software-Defined Networking

Event-Driven Network Programming
Jedidiah McClurg, Hossein Hojjat, Nate Foster, and Pavol Černý
(University of Colorado at Boulder, USA; Cornell University, USA)

Temporal NetKAT
Ryan Beckett, Michael Greenberg, and David Walker
(Princeton University, USA; Pomona College, USA)

SDNRacer: Concurrency Analysis for Software-Defined Networks
Ahmed El-Hassany, Jeremie Miserez, Pavol Bielik, Laurent Vanbever, and Martin Vechev
(ETH Zurich, Switzerland)

Verifying Systems

Rehearsal: A Configuration Verification Tool for Puppet
Rian Shambaugh, Aaron Weiss, and Arjun Guha
(University of Massachusetts at Amherst, USA)

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu
(Yale University, USA)

Verified Peephole Optimizations for CompCert
Eric Mullen, Daryl Zuniga, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)

Types II

Just-in-Time Static Type Checking for Dynamic Languages
Brianna M. Ren and Jeffrey S. Foster
(University of Maryland at College Park, USA)

Types from Data: Making Structured Data First-Class Citizens in F#
Tomas Petricek, Gustavo Guerra, and Don Syme
(University of Cambridge, UK; Microsoft, UK; Microsoft Research, UK)

Automatically Learning Shape Specifications
He Zhu, Gustavo Petri, and Suresh Jagannathan
(Purdue University, USA; University of Paris Diderot, France)

Synthesis II

Synthesizing Transformations on Hierarchically Structured Data
Navid Yaghmazadeh, Christian Klinger, Isil Dillig, and Swarat Chaudhuri
(University of Texas at Austin, USA; University of Freiburg, Germany; Rice University, USA)

Program Synthesis from Polymorphic Refinement Types
Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA)

Parallelism I

Higher-Order and Tuple-Based Massively-Parallel Prefix Sums
Sepideh Maleki, Annie Yang, and Martin Burtscher
(Texas State University, USA)

A Distributed OpenCL Framework using Redundant Computation and Data Replication
Junghyun Kim, Gangwon Jo, Jaehoon Jung, Jungwon Kim, and Jaejin Lee
(Seoul National University, South Korea)

Memory Management

Idle Time Garbage Collection Scheduling
Ulan Degenbaev, Jochen Eisinger, Manfred Ernst, Ross McIlroy, and Hannes Payer
(Google, Germany; Google, USA; Google, UK)

Assessing the Limits of Program-Specific Garbage Collection Performance
Nicholas Jacek, Meng-Chieh Chiu, Benjamin Marlin, and Eliot Moss
(University of Massachusetts at Amherst, USA)

Verification II

Cardinalities and Universal Quantifiers for Verifying Parameterized Systems
Klaus v. Gleissenthall, Nikolaj Bjørner, and Andrey Rybalchenko
(TU Munich, Germany; University of California at San Diego, USA; Microsoft Research, USA; Microsoft Research, UK)

Ivy: Safety Verification by Interactive Generalization
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; Microsoft Research, USA; University of California at Berkeley, USA)

Security

Precise, Dynamic Information Flow for Database-Backed Applications
Jean Yang, Travis Hance, Thomas H. Austin, Armando Solar-Lezama, Cormac Flanagan, and Stephen Chong
(Carnegie Mellon University, USA; Harvard Medical School, USA; Dropbox, USA; San Jose State University, USA; Massachusetts Institute of Technology, USA; University of California at Santa Cruz, USA; Harvard University, USA)

End-to-End Verification of Information-Flow Security for C and Assembly Programs
David Costanzo, Zhong Shao, and Ronghui Gu
(Yale University, USA)

A Design and Verification Methodology for Secure Isolated Regions
Rohit Sinha, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram Rajamani, Sanjit A. Seshia, and Kapil Vaswani
(University of California at Berkeley, USA; Microsoft Research, UK; Microsoft Research, India)

Parallelism II

Transactional Data Structure Libraries
Alexander Spiegelman, Guy Golan-Gueta, and Idit Keidar
(Technion, Israel; Yahoo Research, Israel)

FlexVec: Auto-Vectorization for Irregular Loops
Sara S. Baghsorkhi, Nalini Vasudevan, and Youfeng Wu
(Intel, USA; Google, USA)

Verified Lifting of Stencil Computations
Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, and Armando Solar-Lezama
(Adobe, USA; University of Washington, USA; Massachusetts Institute of Technology, USA)

proc time: 0.68