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 ORCID logo, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall ORCID logo, Robert N. M. Watson, and Peter Sewell ORCID logo
(University of Cambridge, UK)
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)
Polymorphic Type Inference for Machine Code
Matt Noonan, Alexey Loginov, and David Cok
(GrammaTech, USA)
Info

Verification I

Data-Driven Precondition Inference with Learned Features
Saswat Padhi, Rahul Sharma, and Todd Millstein ORCID logo
(University of California at Los Angeles, USA; Stanford University, USA)
Cartesian Hoare Logic for Verifying k-Safety Properties
Marcelo Sousa and Isil Dillig ORCID logo
(University of Oxford, UK; University of Texas at Austin, USA)
Verifying Bit-Manipulations of Floating-Point
Wonyeol Lee ORCID logo, Rahul Sharma, and Alex AikenORCID logo
(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. DonaldsonORCID logo
(Imperial College London, UK)
Lightweight Computation Tree Tracing for Lazy Functional Languages
Maarten Faddegon and Olaf Chitil
(University of Kent, UK)
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)
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)
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 ORCID logo
(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 AikenORCID logo
(Stanford University, USA; VMware, USA)
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)
aec-badge-pldi
Statistical Similarity of Binaries
Yaniv David, Nimrod Partush, and Eran Yahav
(Technion, Israel)
Info

Types I

Accepting Blame for Safe Tunneled Exceptions
Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, and Andrew C. Myers ORCID logo
(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)
aec-badge-pldi
Refinement Types for TypeScript
Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala
(University of California at San Diego, USA)
aec-badge-pldi

Synthesis I

MapReduce Program Synthesis
Calvin Smith and Aws Albarghouthi ORCID logo
(University of Wisconsin-Madison, USA)
Programmatic and Direct Manipulation, Together at Last
Ravi ChughORCID logo, Brian Hempel, Mitchell Spradlin, and Jacob Albers
(University of Chicago, USA)
Info aec-badge-pldi
Fast Synthesis of Fast Collections
Calvin Loncaric, Emina Torlak ORCID logo, and Michael D. ErnstORCID logo
(University of Washington, USA)
Info aec-badge-pldi

Software-Defined Networking

Event-Driven Network Programming
Jedidiah McClurg, Hossein Hojjat, Nate FosterORCID logo, and Pavol Černý
(University of Colorado at Boulder, USA; Cornell University, USA)
aec-badge-pldi
Temporal NetKAT
Ryan Beckett, Michael Greenberg ORCID logo, and David Walker ORCID logo
(Princeton University, USA; Pomona College, USA)
aec-badge-pldi
SDNRacer: Concurrency Analysis for Software-Defined Networks
Ahmed El-Hassany, Jeremie Miserez, Pavol Bielik, Laurent Vanbever, and Martin VechevORCID logo
(ETH Zurich, Switzerland)
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)
aec-badge-pldi
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Hao Chen ORCID logo, Xiongnan (Newman) Wu, Zhong Shao ORCID logo, Joshua Lockerman, and Ronghui Gu
(Yale University, USA)
Verified Peephole Optimizations for CompCert
Eric Mullen, Daryl Zuniga, Zachary Tatlock ORCID logo, 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)
aec-badge-pldi
Types from Data: Making Structured Data First-Class Citizens in F#
Tomas Petricek ORCID logo, 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 ORCID logo
(Purdue University, USA; University of Paris Diderot, France)
aec-badge-pldi

Synthesis II

Synthesizing Transformations on Hierarchically Structured Data
Navid Yaghmazadeh, Christian Klinger, Isil Dillig ORCID logo, 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 ORCID logo
(Massachusetts Institute of Technology, USA)
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)
Info aec-badge-pldi
A Distributed OpenCL Framework using Redundant Computation and Data Replication
Junghyun Kim, Gangwon Jo, Jaehoon Jung ORCID logo, Jungwon Kim, and Jaejin Lee ORCID logo
(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)
aec-badge-pldi
Assessing the Limits of Program-Specific Garbage Collection Performance
Nicholas Jacek, Meng-Chieh Chiu, Benjamin Marlin, and Eliot Moss ORCID logo
(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 ORCID logo, and Sharon Shoham ORCID logo
(Tel Aviv University, Israel; Microsoft Research, USA; University of California at Berkeley, USA)
aec-badge-pldi

Security

Precise, Dynamic Information Flow for Database-Backed Applications
Jean Yang, Travis Hance, Thomas H. Austin, Armando Solar-Lezama ORCID logo, Cormac Flanagan, and Stephen Chong ORCID logo
(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)
aec-badge-pldi
End-to-End Verification of Information-Flow Security for C and Assembly Programs
David Costanzo, Zhong Shao ORCID logo, and Ronghui Gu
(Yale University, USA)
aec-badge-pldi
A Design and Verification Methodology for Secure Isolated Regions
Rohit Sinha, Manuel Costa, Akash LalORCID logo, Nuno P. Lopes, Sriram Rajamani ORCID logo, Sanjit A. Seshia, and Kapil Vaswani
(University of California at Berkeley, USA; Microsoft Research, UK; Microsoft Research, India)
aec-badge-pldi

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 ORCID logo
(Adobe, USA; University of Washington, USA; Massachusetts Institute of Technology, USA)

proc time: 0.84