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

Title Page
Message from the Chairs
Organization
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)
Publisher's Version Article Search Info
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)
Publisher's Version Article Search
Polymorphic Type Inference for Machine Code
Matt Noonan, Alexey Loginov, and David Cok
(GrammaTech, USA)
Publisher's Version Article Search Info

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)
Publisher's Version Article Search
Cartesian Hoare Logic for Verifying k-Safety Properties
Marcelo Sousa and Isil Dillig
(University of Oxford, UK; University of Texas at Austin, USA)
Publisher's Version Article Search
Verifying Bit-Manipulations of Floating-Point
Wonyeol Lee, Rahul Sharma, and Alex Aiken
(Stanford University, USA)
Publisher's Version Article Search

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)
Publisher's Version Article Search
Exposing Errors Related to Weak Memory in GPU Applications
Tyler Sorensen and Alastair F. Donaldson
(Imperial College London, UK)
Publisher's Version Article Search
Lightweight Computation Tree Tracing for Lazy Functional Languages
Maarten Faddegon and Olaf Chitil
(University of Kent, UK)
Publisher's Version Article Search Artifacts Available aec-badge-pldi

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)
Publisher's Version Article Search
GreenWeb: Language Extensions for Energy-Efficient Mobile Web Computing
Yuhao Zhu and Vijay Janapa Reddi
(University of Texas at Austin, USA)
Publisher's Version Article Search
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)
Publisher's Version Article Search

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)
Publisher's Version Article Search aec-badge-pldi
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)
Publisher's Version Article Search
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)
Publisher's Version Article Search

Parsing and Compilation

On the Complexity and Performance of Parsing with Derivatives
Michael D. Adams, Celeste Hollenbeck, and Matthew Might
(University of Utah, USA)
Publisher's Version Article Search

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)
Publisher's Version Article Search Info
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)
Publisher's Version Article Search aec-badge-pldi
Statistical Similarity of Binaries
Yaniv David, Nimrod Partush, and Eran Yahav
(Technion, Israel)
Publisher's Version Article Search Info

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)
Publisher's Version Article Search
Occurrence Typing Modulo Theories
Andrew M. Kent, David Kempe, and Sam Tobin-Hochstadt
(Indiana University, USA)
Publisher's Version Article Search aec-badge-pldi
Refinement Types for TypeScript
Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala
(University of California at San Diego, USA)
Publisher's Version Article Search aec-badge-pldi

Synthesis I

MapReduce Program Synthesis
Calvin Smith and Aws Albarghouthi
(University of Wisconsin-Madison, USA)
Publisher's Version Article Search
Programmatic and Direct Manipulation, Together at Last
Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers
(University of Chicago, USA)
Publisher's Version Article Search Info aec-badge-pldi
Fast Synthesis of Fast Collections
Calvin Loncaric, Emina Torlak, and Michael D. Ernst
(University of Washington, USA)
Publisher's Version Article Search Info aec-badge-pldi

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)
Publisher's Version Article Search aec-badge-pldi
Temporal NetKAT
Ryan Beckett, Michael Greenberg, and David Walker
(Princeton University, USA; Pomona College, USA)
Publisher's Version Article Search Artifacts Available aec-badge-pldi
SDNRacer: Concurrency Analysis for Software-Defined Networks
Ahmed El-Hassany, Jeremie Miserez, Pavol Bielik, Laurent Vanbever, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version Article Search aec-badge-pldi

Verifying Systems

Rehearsal: A Configuration Verification Tool for Puppet
Rian Shambaugh, Aaron Weiss, and Arjun Guha
(University of Massachusetts at Amherst, USA)
Publisher's Version Article Search aec-badge-pldi
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)
Publisher's Version Article Search
Verified Peephole Optimizations for CompCert
Eric Mullen, Daryl Zuniga, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)
Publisher's Version Article Search

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)
Publisher's Version Article Search aec-badge-pldi
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)
Publisher's Version Article Search
Automatically Learning Shape Specifications
He Zhu, Gustavo Petri, and Suresh Jagannathan
(Purdue University, USA; University of Paris Diderot, France)
Publisher's Version Article Search aec-badge-pldi

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)
Publisher's Version Article Search
Program Synthesis from Polymorphic Refinement Types
Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search aec-badge-pldi

Parallelism I

Higher-Order and Tuple-Based Massively-Parallel Prefix Sums
Sepideh Maleki, Annie Yang, and Martin Burtscher
(Texas State University, USA)
Publisher's Version Article Search Info aec-badge-pldi
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)
Publisher's Version Article Search

Memory Management

Idle Time Garbage Collection Scheduling
Ulan Degenbaev, Jochen Eisinger, Manfred Ernst, Ross McIlroy, and Hannes Payer
(Google, Germany; Google, USA; Google, UK)
Publisher's Version Article Search Artifacts Available aec-badge-pldi
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)
Publisher's Version Article Search

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)
Publisher's Version Article Search
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)
Publisher's Version Article Search aec-badge-pldi

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)
Publisher's Version Article Search aec-badge-pldi
End-to-End Verification of Information-Flow Security for C and Assembly Programs
David Costanzo, Zhong Shao, and Ronghui Gu
(Yale University, USA)
Publisher's Version Article Search aec-badge-pldi
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)
Publisher's Version Article Search aec-badge-pldi

Parallelism II

Transactional Data Structure Libraries
Alexander Spiegelman, Guy Golan-Gueta, and Idit Keidar
(Technion, Israel; Yahoo Research, Israel)
Publisher's Version Article Search
FlexVec: Auto-Vectorization for Irregular Loops
Sara S. Baghsorkhi, Nalini Vasudevan, and Youfeng Wu
(Intel, USA; Google, USA)
Publisher's Version Article Search
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)
Publisher's Version Article Search

proc time: 0.31