Frontmatter

Research Papers

Distinguished Papers
Mon, Jun 15, 09:00 - 11:00 (Chair: Steve Blackburn)

Automatically Improving Accuracy for Floating Point Expressions
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock 
(University of Washington, USA)

aec-badge-pldi

Diagnosing Type Errors with Class
Danfeng Zhang, Andrew C. Myers , Dimitrios Vytiniotis, and Simon Peyton-Jones
(Cornell University, USA; Microsoft Research, UK)

Provably Correct Peephole Optimizations with Alive
Nuno P. Lopes, David Menendez, Santosh Nagarakatte , and John Regehr 
(Microsoft Research, UK; Rutgers University, USA; University of Utah, USA)

Video

Correctness
Mon, Jun 15, 14:00 - 15:40 (Chair: Jens Palsberg)

Algorithmic Debugging of Real-World Haskell Programs: Deriving Dependencies from the Cost Centre Stack
Maarten Faddegon and Olaf Chitil
(University of Kent, UK)

Video aec-badge-pldi

Light: Replay via Tightly Bounded Recording
Peng Liu, Xiangyu Zhang , Omer Tripp, and Yunhui Zheng
(Purdue University, USA; IBM Research, USA)

Many-Core Compiler Fuzzing
Christopher Lidbury, Andrei Lascu, Nathan Chong, and Alastair F. Donaldson
(Imperial College London, UK; University College London, UK)

aec-badge-pldi

Verification
Mon, Jun 15, 14:00 - 15:40 (Chair: Nate Foster)

Mechanized Verification of Fine-Grained Concurrent Programs
Ilya Sergey, Aleksandar Nanevski , and Anindya Banerjee 
(IMDEA Software Institute, Spain)

Video Info aec-badge-pldi

Verification of Producer-Consumer Synchronization in GPU Programs
Rahul Sharma, Michael Bauer, and Alex Aiken 
(Stanford University, USA; NVIDIA Research, USA)

Video Info aec-badge-pldi

Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
Peter Gammie, Antony L. Hosking, and Kai Engelhardt
(NICTA, Australia; Purdue University, USA; UNSW, Australia)

Video aec-badge-pldi

Verifying Read-Copy-Update in a Logic for Weak Memory
Joseph Tassarotti, Derek Dreyer , and Viktor Vafeiadis 
(Carnegie Mellon University, USA; MPI-SWS, Germany)

Optimization
Mon, Jun 15, 16:00 - 17:15 (Chair: Michelle Mills Strout)

LaminarIR: Compile-Time Queues for Structured Streams
Yousun Ko, Bernd Burgstaller, and Bernhard Scholz
(Yonsei University, South Korea; University of Sydney, Australia)

Info

TOPLAS
Mon, Jun 15, 17:15 - 17:40 (Chair: Michelle Mills Strout)

Concurrency I
Mon, Jun 15, 16:00 - 17:40 (Chair: Santosh Nagarakatte)

Asynchronous Programming, Analysis and Testing with State Machines
Pantazis Deligiannis, Alastair F. Donaldson , Jeroen Ketema, Akash Lal , and Paul Thomson
(Imperial College London, UK; Microsoft Research, India)

aec-badge-pldi

Stateless Model Checking Concurrent Programs with Maximal Causality Reduction
Jeff Huang 
(Texas A&M University, USA)

Video Info

Synthesizing Racy Tests
Malavika Samak, Murali Krishna Ramanathan, and Suresh Jagannathan 
(Indian Institute of Science, India; Purdue University, USA)

aec-badge-pldi

The Push/Pull Model of Transactions
Eric Koskinen and Matthew Parkinson 
(IBM Research, USA; Microsoft Research, UK)

Synthesis I
Tue, Jun 16, 09:15 - 10:55 (Chair: Kathleen Fisher)

Efficient Synthesis of Network Updates
Jedidiah McClurg, Hossein Hojjat, Pavol Černý, and Nate Foster 
(University of Colorado at Boulder, USA; Cornell University, USA)

Video aec-badge-pldi

FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples
Daniel W. Barowy, Sumit Gulwani , Ted Hart, and Benjamin Zorn
(University of Massachusetts at Amherst, USA; Microsoft Research, USA)

aec-badge-pldi

Synthesizing Data Structure Transformations from Input-Output Examples
John K. Feser, Swarat Chaudhuri, and Isil Dillig 
(Rice University, USA; University of Texas at Austin, USA)

Concurrency II
Tue, Jun 16, 09:15 - 10:55 (Chair: Suresh Jagannathan)

Composing Concurrency Control
Ofri Ziv, Alex Aiken , Guy Golan-Gueta, G. Ramalingam, and Mooly Sagiv
(Tel Aviv University, Israel; Stanford University, USA; Microsoft Research, India)

Video

Dynamic Partial Order Reduction for Relaxed Memory Models
Naling Zhang, Markus Kusano, and Chao Wang
(Virginia Tech, USA)

Video

Monitoring Refinement via Symbolic Reasoning
Michael Emmi, Constantin Enea, and Jad Hamza
(IMDEA Software Institute, Spain; University of Paris Diderot, France)

aec-badge-pldi

Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications
Stephen Longfield, Brittany Nkounkou, Rajit Manohar, and Ross Tate 
(Cornell University, USA)

Info aec-badge-pldi

Analysis
Tue, Jun 16, 14:00 - 15:40 (Chair: Yannis Smaragdakis)

DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs
Akash Lal  and Shaz Qadeer
(Microsoft Research, India; Microsoft Research, USA)

Exploring and Enforcing Security Guarantees via Program Dependence Graphs
Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong 
(Harvard University, USA; MIT Lincoln Laboratory, USA)

Making Numerical Program Analysis Fast
Gagandeep Singh, Markus Püschel, and Martin Vechev 
(ETH Zurich, Switzerland)

Video Info aec-badge-pldi

Tree Dependence Analysis
Yusheng Weijiang, Shruthi Balakrishna, Jianqiao Liu, and Milind Kulkarni 
(Purdue University, USA)

aec-badge-pldi

Semantics I
Tue, Jun 16, 14:00 - 15:40 (Chair: Hans-J. Boehm)

A Formal C Memory Model Supporting Integer-Pointer Casts
Jeehoon Kang, Chung-Kil Hur , William Mansky, Dmitri Garbuzov, Steve Zdancewic , and Viktor Vafeiadis 
(Seoul National University, South Korea; University of Pennsylvania, USA; MPI-SWS, Germany)

Video Info aec-badge-pldi

Defining the Undefinedness of C
Chris Hathhorn, Chucky Ellison, and Grigore Roşu 
(University of Missouri, USA; University of Illinois at Urbana-Champaign, USA)

KJS: A Complete Formal Semantics of JavaScript
Daejun Park, Andrei Stefănescu, and Grigore Roşu 
(University of Illinois at Urbana-Champaign, USA)

aec-badge-pldi

Verdi: A Framework for Implementing and Formally Verifying Distributed Systems
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock , Xi Wang, Michael D. Ernst , and Thomas Anderson
(University of Washington, USA)

aec-badge-pldi

Performance
Wed, Jun 17, 09:15 - 10:55 (Chair: Mary Hall)

Static Detection of Asymptotic Performance Bugs in Collection Traversals
Oswaldo Olivo, Isil Dillig , and Calvin Lin
(University of Texas at Austin, USA)

Autotuning Algorithmic Choice for Input Sensitivity
Yufei Ding, Jason Ansel, Kalyan Veeramachaneni, Xipeng Shen , Una-May O’Reilly , and Saman Amarasinghe 
(North Carolina State University, USA; Massachusetts Institute of Technology, USA)

Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code
Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe 
(Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA)

Info

Profile-Guided Meta-Programming
William J. Bowman , Swaha Miller, Vincent St-Amour, and R. Kent Dybvig
(Northeastern University, USA; Cisco Systems, USA)

Semantics II
Wed, Jun 17, 09:15 - 10:55 (Chair: Robby Findler)

Declarative Programming over Eventually Consistent Data Stores
KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan 
(University of Cambridge, UK; Purdue University, USA)

Video Info aec-badge-pldi

Blame and Coercion: Together Again for the First Time
Jeremy Siek, Peter Thiemann , and Philip Wadler 
(Indiana University, USA; University of Freiburg, Germany; University of Edinburgh, UK)

Lightweight, Flexible Object-Oriented Generics
Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, and Andrew C. Myers 
(Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA)

aec-badge-pldi

Relatively Complete Counterexamples for Higher-Order Programs
Phúc C. Nguyễn and David Van Horn 
(University of Maryland, USA)

aec-badge-pldi

Logic
Wed, Jun 17, 14:00 - 15:40 (Chair: Madhusudan Parthasarathy)

Automatic Induction Proofs of Data-Structures in Imperative Programs
Duc-Hiep Chu, Joxan Jaffar , and Minh-Thai Trinh
(National University of Singapore, Singapore)

Compositional Certified Resource Bounds
Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao 
(Yale University, USA)

Video Info aec-badge-pldi

Termination and Non-termination Specification Inference
Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin 
(National University of Singapore, Singapore; Teesside University, UK; Shenzhen University, China)

Video Info aec-badge-pldi

Parallelism
Wed, Jun 17, 14:00 - 15:40 (Chair: Sara Baghsorkhi)

Celebrating Diversity: A Mixture of Experts Approach for Runtime Mapping in Dynamic Environments
Murali Krishna Emani and Michael O'Boyle 
(University of Edinburgh, UK)

Efficient Execution of Recursive Programs on Commodity Vector Hardware
Bin Ren, Youngjoon Jo, Sriram Krishnamoorthy, Kunal Agrawal, and Milind Kulkarni 
(Pacific Northwest National Laboratory, USA; Purdue University, USA; Washington University at St. Louis, USA)

aec-badge-pldi

Loop and Data Transformations for Sparse Matrix Code
Anand Venkat, Mary Hall , and Michelle Strout
(University of Utah, USA; Colorado State University, USA)

Potpourri
Wed, Jun 17, 16:00 - 17:40 (Chair: Tiark Rompf)

Zero-Overhead Metaprogramming: Reflection and Metaobject Protocols Fast and without Compromises
Stefan Marr, Chris Seaton, and Stéphane Ducasse 
(INRIA, France; Oracle Labs, USA; University of Manchester, UK)

Info aec-badge-pldi

Finding Counterexamples from Parsing Conflicts
Chinawat Isradisaikul and Andrew C. Myers 
(Cornell University, USA)

Video Info

Interactive Parser Synthesis by Example
Alan Leung, John Sarracino, and Sorin Lerner 
(University of California at San Diego, USA)

aec-badge-pldi

Synthesis II
Wed, Jun 17, 16:00 - 17:40 (Chair: Isil Dillig)

Concurrency Debugging with Differential Schedule Projections
Nuno Machado, Brandon Lucia, and Luís Rodrigues
(Universidade de Lisboa, Portugal; Carnegie Mellon University, USA)

Video aec-badge-pldi

Synthesis of Machine Code from Semantics
Venkatesh Srinivasan and Thomas Reps 
(University of Wisconsin-Madison, USA; GrammaTech, USA)

Synthesis of Ranking Functions using Extremal Counterexamples
Laure Gonnord , David Monniaux, and Gabriel Radanne
(Claude Bernard University Lyon 1, France; LIP, France; University of Grenoble, France; VERIMAG, France; University of Paris Diderot, France)

Type-and-Example-Directed Program Synthesis
Peter-Michael Osera and Steve Zdancewic 
(University of Pennsylvania, USA)

aec-badge-pldi

proc time: 1.07