PLDI 2018 – Proceedings

Frontmatter

Web Pages

Verifying That Web Pages Have Accessible Layout
Pavel Panchekha, Adam T. Geller, Michael D. Ernst, Zachary Tatlock, and Shoaib Kamil
(University of Washington, USA; Adobe Research, USA)


@InProceedings{PLDI18p1, author = {Pavel Panchekha and Adam T. Geller and Michael D. Ernst and Zachary Tatlock and Shoaib Kamil}, title = {Verifying That Web Pages Have Accessible Layout}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1-0}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

BLeak: Automatically Debugging Memory Leaks in Web Applications
John Vilk and Emery D. Berger
(University of Massachusetts at Amherst, USA)


@InProceedings{PLDI18p18, author = {John Vilk and Emery D. Berger}, title = {BLeak: Automatically Debugging Memory Leaks in Web Applications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {18-17}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

Putting in All the Stops: Execution Control for JavaScript
Samuel Baxter, Rachit Nigam, Joe Gibbs Politz, Shriram Krishnamurthi, and Arjun Guha
(University of Massachusetts at Amherst, USA; University of California at San Diego, USA; Brown University, USA)


@InProceedings{PLDI18p35, author = {Samuel Baxter and Rachit Nigam and Joe Gibbs Politz and Shriram Krishnamurthi and Arjun Guha}, title = {Putting in All the Stops: Execution Control for JavaScript}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {35-34}, doi = {}, year = {2018}, } Artifacts Functional

Emerging Hardware

Persistency for Synchronization-Free Regions
Vaibhav Gogte, Stephan Diestelhorst, William Wang, Satish Narayanasamy, Peter M. Chen, and Thomas F. Wenisch
(University of Michigan, USA; ARM Research, UK)


@InProceedings{PLDI18p52, author = {Vaibhav Gogte and Stephan Diestelhorst and William Wang and Satish Narayanasamy and Peter M. Chen and Thomas F. Wenisch}, title = {Persistency for Synchronization-Free Regions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {52-51}, doi = {}, year = {2018}, }

Write-Rationing Garbage Collection for Hybrid Memories
Shoaib Akram, Jennifer B. Sartor, Kathryn S. McKinley, and Lieven Eeckhout
(Ghent University, Belgium; Vrije Universiteit Brussel, Belgium; Google, USA)


@InProceedings{PLDI18p69, author = {Shoaib Akram and Jennifer B. Sartor and Kathryn S. McKinley and Lieven Eeckhout}, title = {Write-Rationing Garbage Collection for Hybrid Memories}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {69-68}, doi = {}, year = {2018}, }

Mapping Spiking Neural Networks onto a Manycore Neuromorphic Architecture
Chit-Kwan Lin, Andreas Wild, Gautham N. Chinya, Tsung-Han Lin, Mike Davies, and Hong Wang
(Intel Labs, USA)


@InProceedings{PLDI18p86, author = {Chit-Kwan Lin and Andreas Wild and Gautham N. Chinya and Tsung-Han Lin and Mike Davies and Hong Wang}, title = {Mapping Spiking Neural Networks onto a Manycore Neuromorphic Architecture}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {86-85}, doi = {}, year = {2018}, }

Concurrency and Termination

Static Serializability Analysis for Causal Consistency
Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev
(ETH Zurich, Switzerland)


@InProceedings{PLDI18p103, author = {Lucas Brutschy and Dimitar Dimitrov and Peter Müller and Martin Vechev}, title = {Static Serializability Analysis for Causal Consistency}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {103-102}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs
Peizun Liu and Thomas Wahl
(Northeastern University, USA)


@InProceedings{PLDI18p120, author = {Peizun Liu and Thomas Wahl}, title = {CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {120-119}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

Symbolic Reasoning for Automatic Signal Placement
Kostas Ferles, Jacob Van Geffen, Isil Dillig, and Yannis Smaragdakis
(University of Texas at Austin, USA; University of Athens, Greece)


@InProceedings{PLDI18p137, author = {Kostas Ferles and Jacob Van Geffen and Isil Dillig and Yannis Smaragdakis}, title = {Symbolic Reasoning for Automatic Signal Placement}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {137-136}, doi = {}, year = {2018}, }

Advanced Automata-Based Algorithms for Program Termination Checking
Yu-Fang Chen, Matthias Heizmann, Ondřej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, and Lijun Zhang
(Academia Sinica, Taiwan; National Taipei University, Taiwan; University of Freiburg, Germany; Brno University of Technology, Czechia; Institute of Software at Chinese Academy of Sciences, China)


@InProceedings{PLDI18p154, author = {Yu-Fang Chen and Matthias Heizmann and Ondřej Lengál and Yong Li and Ming-Hsien Tsai and Andrea Turrini and Lijun Zhang}, title = {Advanced Automata-Based Algorithms for Program Termination Checking}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {154-153}, doi = {}, year = {2018}, }

Dynamic Techniques

HHVM JIT: A Profile-Guided, Region-Based Compiler for PHP and Hack
Guilherme Ottoni
(Facebook, USA)


@InProceedings{PLDI18p171, author = {Guilherme Ottoni}, title = {HHVM JIT: A Profile-Guided, Region-Based Compiler for PHP and Hack}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {171-170}, doi = {}, year = {2018}, }

On-Stack Replacement, Distilled
Daniele Cono D'Elia and Camil Demetrescu
(Sapienza University of Rome, Italy)


@InProceedings{PLDI18p188, author = {Daniele Cono D'Elia and Camil Demetrescu}, title = {On-Stack Replacement, Distilled}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {188-187}, doi = {}, year = {2018}, }

EffectiveSan: Type and Memory Error Detection using Dynamically Typed C/C++
Gregory J. Duck and Roland H. C. Yap
(National University of Singapore, Singapore)


@InProceedings{PLDI18p205, author = {Gregory J. Duck and Roland H. C. Yap}, title = {EffectiveSan: Type and Memory Error Detection using Dynamically Typed C/C++}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {205-204}, doi = {}, year = {2018}, }

Calling-to-Reference Context Translation via Constraint-Guided CFL-Reachability
Cheng Cai, Qirun Zhang, Zhiqiang Zuo, Khanh Nguyen, Guoqing Xu, and Zhendong Su
(University of California at Irvine, USA; University of California at Davis, USA; Nanjing University, China)


@InProceedings{PLDI18p222, author = {Cheng Cai and Qirun Zhang and Zhiqiang Zuo and Khanh Nguyen and Guoqing Xu and Zhendong Su}, title = {Calling-to-Reference Context Translation via Constraint-Guided CFL-Reachability}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {222-221}, doi = {}, year = {2018}, }

Transactions and Races

The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
Nathan Chong, Tyler Sorensen, and John Wickerson
(ARM, UK; Imperial College London, UK)


@InProceedings{PLDI18p239, author = {Nathan Chong and Tyler Sorensen and John Wickerson}, title = {The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {239-238}, doi = {}, year = {2018}, } Artifacts Functional

MixT: A Language for Mixing Consistency in Geodistributed Transactions
Matthew Milano and Andrew C. Myers
(Cornell University, USA)


@InProceedings{PLDI18p256, author = {Matthew Milano and Andrew C. Myers}, title = {MixT: A Language for Mixing Consistency in Geodistributed Transactions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {256-255}, doi = {}, year = {2018}, }

Bounding Data Races in Space and Time
Stephen Dolan, KC Sivaramakrishnan, and Anil Madhavapeddy
(University of Cambridge, UK)


@InProceedings{PLDI18p273, author = {Stephen Dolan and KC Sivaramakrishnan and Anil Madhavapeddy}, title = {Bounding Data Races in Space and Time}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {273-272}, doi = {}, year = {2018}, } Artifacts Functional

Floats and Maps

Finding Root Causes of Floating Point Error
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, and Zachary Tatlock
(University of California at San Diego, USA; University of Washington, USA)


@InProceedings{PLDI18p290, author = {Alex Sanchez-Stern and Pavel Panchekha and Sorin Lerner and Zachary Tatlock}, title = {Finding Root Causes of Floating Point Error}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {290-289}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

Ryū: Fast Float-to-String Conversion
Ulf Adams
(Google, Germany)


@InProceedings{PLDI18p307, author = {Ulf Adams}, title = {Ryū: Fast Float-to-String Conversion}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {307-306}, doi = {}, year = {2018}, } Artifacts Functional

To-Many or To-One? All-in-One! Efficient Purely Functional Multi-maps with Type-Heterogeneous Hash-Tries
Michael J. Steindorfer and Jurgen J. Vinju
(Delft University of Technology, Netherlands; CWI, Netherlands; Eindhoven University of Technology, Netherlands)


@InProceedings{PLDI18p324, author = {Michael J. Steindorfer and Jurgen J. Vinju}, title = {To-Many or To-One? All-in-One! Efficient Purely Functional Multi-maps with Type-Heterogeneous Hash-Tries}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {324-323}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

Multicore and More

Spatial: A Language and Compiler for Application Accelerators
David Koeplinger, Matthew Feldman, Raghu Prabhakar, Yaqi Zhang, Stefan Hadjis, Ruben Fiszel, Tian Zhao, Luigi Nardi, Ardavan Pedram, Christos Kozyrakis, and Kunle Olukotun
(Stanford University, USA; EPFL, Switzerland)


@InProceedings{PLDI18p341, author = {David Koeplinger and Matthew Feldman and Raghu Prabhakar and Yaqi Zhang and Stefan Hadjis and Ruben Fiszel and Tian Zhao and Luigi Nardi and Ardavan Pedram and Christos Kozyrakis and Kunle Olukotun}, title = {Spatial: A Language and Compiler for Application Accelerators}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {341-340}, doi = {}, year = {2018}, }

Enhancing Computation-to-Core Assignment with Physical Location Information
Orhan Kislal, Jagadish Kotra, Xulong Tang, Mahmut Taylan Kandemir, and Myoungsoo Jung
(Pennsylvania State University, USA; Yonsei University, South Korea)


@InProceedings{PLDI18p358, author = {Orhan Kislal and Jagadish Kotra and Xulong Tang and Mahmut Taylan Kandemir and Myoungsoo Jung}, title = {Enhancing Computation-to-Core Assignment with Physical Location Information}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {358-357}, doi = {}, year = {2018}, }

SWOOP: Software-Hardware Co-design for Non-speculative, Execute-Ahead, In-Order Cores
Kim-Anh Tran, Alexandra Jimborean, Trevor E. Carlson, Konstantinos Koukos, Magnus Själander, and Stefanos Kaxiras
(Uppsala University, Sweden; National University of Singapore, Singapore; NTNU, Norway)


@InProceedings{PLDI18p375, author = {Kim-Anh Tran and Alexandra Jimborean and Trevor E. Carlson and Konstantinos Koukos and Magnus Själander and Stefanos Kaxiras}, title = {SWOOP: Software-Hardware Co-design for Non-speculative, Execute-Ahead, In-Order Cores}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {375-374}, doi = {}, year = {2018}, }

Concurrency Debugging

iReplayer: In-situ and Identical Record-and-Replay for Multithreaded Applications
Hongyu Liu, Sam Silvestro, Wei Wang, Chen Tian, and Tongping Liu
(University of Texas at San Antonio, USA; Huawei Lab, USA)


@InProceedings{PLDI18p392, author = {Hongyu Liu and Sam Silvestro and Wei Wang and Chen Tian and Tongping Liu}, title = {iReplayer: In-situ and Identical Record-and-Replay for Multithreaded Applications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {392-391}, doi = {}, year = {2018}, }

D4: Fast Concurrency Debugging with Parallel Differential Analysis
Bozhen Liu and Jeff Huang
(Texas A&M University, USA)


@InProceedings{PLDI18p409, author = {Bozhen Liu and Jeff Huang}, title = {D4: Fast Concurrency Debugging with Parallel Differential Analysis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {409-408}, doi = {}, year = {2018}, }

High-Coverage, Unbounded Sound Predictive Race Detection
Jake Roemer, Kaan Genç, and Michael D. Bond
(Ohio State University, USA)


@InProceedings{PLDI18p426, author = {Jake Roemer and Kaan Genç and Michael D. Bond}, title = {High-Coverage, Unbounded Sound Predictive Race Detection}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {426-425}, doi = {}, year = {2018}, } Artifacts Functional

CURD: A Dynamic CUDA Race Detector
Yuanfeng Peng, Vinod Grover, and Joseph Devietti
(University of Pennsylvania, USA; NVIDIA, USA)


@InProceedings{PLDI18p443, author = {Yuanfeng Peng and Vinod Grover and Joseph Devietti}, title = {CURD: A Dynamic CUDA Race Detector}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {443-442}, doi = {}, year = {2018}, }

Synthesis and Learning

A General Path-Based Representation for Predicting Program Properties
Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav
(Technion, Israel; University of Washington, USA)


@InProceedings{PLDI18p460, author = {Uri Alon and Meital Zilberstein and Omer Levy and Eran Yahav}, title = {A General Path-Based Representation for Predicting Program Properties}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {460-459}, doi = {}, year = {2018}, }

Program Synthesis using Conflict-Driven Learning
Yu Feng, Ruben Martins, Osbert Bastani, and Isil Dillig
(University of Texas at Austin, USA; Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA)


@InProceedings{PLDI18p477, author = {Yu Feng and Ruben Martins and Osbert Bastani and Isil Dillig}, title = {Program Synthesis using Conflict-Driven Learning}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {477-476}, doi = {}, year = {2018}, }

Accelerating Search-Based Program Synthesis using Learned Probabilistic Models
Woosuk Lee, Kihong Heo, Rajeev Alur, and Mayur Naik
(University of Pennsylvania, USA)


@InProceedings{PLDI18p494, author = {Woosuk Lee and Kihong Heo and Rajeev Alur and Mayur Naik}, title = {Accelerating Search-Based Program Synthesis using Learned Probabilistic Models}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {494-493}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

Inferring Crypto API Rules from Code Changes
Rumen Paletov, Petar Tsankov, Veselin Raychev, and Martin Vechev
(ETH Zurich, Switzerland; DeepCode, Switzerland)


@InProceedings{PLDI18p511, author = {Rumen Paletov and Petar Tsankov and Veselin Raychev and Martin Vechev}, title = {Inferring Crypto API Rules from Code Changes}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {511-510}, doi = {}, year = {2018}, }

Programming-Student Feedback

Automated Clustering and Program Repair for Introductory Programming Assignments
Sumit Gulwani, Ivan Radiček, and Florian Zuleger
(Microsoft, USA; Vienna University of Technology, Austria)


@InProceedings{PLDI18p528, author = {Sumit Gulwani and Ivan Radiček and Florian Zuleger}, title = {Automated Clustering and Program Repair for Introductory Programming Assignments}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {528-527}, doi = {}, year = {2018}, }

Search, Align, and Repair: Data-Driven Feedback Generation for Introductory Programming Exercises
Ke Wang, Rishabh Singh, and Zhendong Su
(University of California at Davis, USA; Microsoft Research, USA)


@InProceedings{PLDI18p545, author = {Ke Wang and Rishabh Singh and Zhendong Su}, title = {Search, Align, and Repair: Data-Driven Feedback Generation for Introductory Programming Exercises}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {545-544}, doi = {}, year = {2018}, }

Analyzing Probabilistic Programs

Bounded Expectations: Resource Analysis for Probabilistic Programs
Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann
(Carnegie Mellon University, USA; Yale University, USA)


@InProceedings{PLDI18p562, author = {Van Chan Ngo and Quentin Carbonneaux and Jan Hoffmann}, title = {Bounded Expectations: Resource Analysis for Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {562-561}, doi = {}, year = {2018}, } Artifacts Functional

PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs
Di Wang, Jan Hoffmann, and Thomas Reps
(Carnegie Mellon University, USA; University of Wisconsin, USA; GrammaTech, USA)


@InProceedings{PLDI18p579, author = {Di Wang and Jan Hoffmann and Thomas Reps}, title = {PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {579-578}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

Optimization and Locality

Polyhedral Auto-transformation with No Integer Linear Programming
Aravind Acharya, Uday Bondhugula, and Albert Cohen
(Indian Institute of Science, India; Inria, France; ENS, France)


@InProceedings{PLDI18p596, author = {Aravind Acharya and Uday Bondhugula and Albert Cohen}, title = {Polyhedral Auto-transformation with No Integer Linear Programming}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {596-595}, doi = {}, year = {2018}, }

Partial Control-Flow Linearization
Simon Moll and Sebastian Hack
(Saarland University, Germany)


@InProceedings{PLDI18p613, author = {Simon Moll and Sebastian Hack}, title = {Partial Control-Flow Linearization}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {613-612}, doi = {}, year = {2018}, }

Locality Analysis through Static Parallel Sampling
Dong Chen, Fangzhou Liu, Chen Ding, and Sreepathi Pai
(University of Rochester, USA)


@InProceedings{PLDI18p630, author = {Dong Chen and Fangzhou Liu and Chen Ding and Sreepathi Pai}, title = {Locality Analysis through Static Parallel Sampling}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {630-629}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

Inference for Probabilistic Programs

Incremental Inference for Probabilistic Programs
Marco Cusumano-Towner, Benjamin Bichsel, Timon Gehr, Martin Vechev, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA; ETH Zurich, Switzerland)


@InProceedings{PLDI18p647, author = {Marco Cusumano-Towner and Benjamin Bichsel and Timon Gehr and Martin Vechev and Vikash K. Mansinghka}, title = {Incremental Inference for Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {647-646}, doi = {}, year = {2018}, } Artifacts Functional

Bayonet: Probabilistic Inference for Networks
Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin Vechev
(ETH Zurich, Switzerland; University of Illinois at Urbana-Champaign, USA)


@InProceedings{PLDI18p664, author = {Timon Gehr and Sasa Misailovic and Petar Tsankov and Laurent Vanbever and Pascal Wiesmann and Martin Vechev}, title = {Bayonet: Probabilistic Inference for Networks}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {664-663}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

Probabilistic Programming with Programmable Inference
Vikash K. Mansinghka, Ulrich Schaechtle, Shivam Handa, Alexey Radul, Yutian Chen, and Martin Rinard
(Massachusetts Institute of Technology, USA; Google Deepmind, UK)


@InProceedings{PLDI18p681, author = {Vikash K. Mansinghka and Ulrich Schaechtle and Shivam Handa and Alexey Radul and Yutian Chen and Martin Rinard}, title = {Probabilistic Programming with Programmable Inference}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {681-680}, doi = {}, year = {2018}, }

Verification

VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models
Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer
(Carnegie Mellon University, USA; Chalmers University of Technology, Sweden)


@InProceedings{PLDI18p698, author = {Brandon Bohrer and Yong Kiam Tan and Stefan Mitsch and Magnus O. Myreen and André Platzer}, title = {VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {698-697}, doi = {}, year = {2018}, } Artifacts Functional

Crellvm: Verified Credible Compilation for LLVM
Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, and Kwangkeun Yi
(Seoul National University, South Korea; Massachusetts Institute of Technology, USA)


@InProceedings{PLDI18p715, author = {Jeehoon Kang and Yoonseung Kim and Youngju Song and Juneyoung Lee and Sanghoon Park and Mark Dongyeon Shin and Yonghyun Kim and Sungkeun Cho and Joonwon Choi and Chung-Kil Hur and Kwangkeun Yi}, title = {Crellvm: Verified Credible Compilation for LLVM}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {715-714}, doi = {}, year = {2018}, } Artifacts Functional

Certified Concurrent Abstraction Layers
Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro
(Yale University, USA; Microsoft Research, USA)


@InProceedings{PLDI18p732, author = {Ronghui Gu and Zhong Shao and Jieung Kim and Xiongnan (Newman) Wu and Jérémie Koenig and Vilhelm Sjöberg and Hao Chen and David Costanzo and Tahina Ramananandro}, title = {Certified Concurrent Abstraction Layers}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {732-731}, doi = {}, year = {2018}, } Artifacts Functional

Modularity for Decidability of Deductive Verification with Applications to Distributed Systems
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos
(Tel Aviv University, Israel; University of California at Los Angeles, USA; Microsoft Research, USA; University of Washington, USA)


@InProceedings{PLDI18p749, author = {Marcelo Taube and Giuliano Losa and Kenneth L. McMillan and Oded Padon and Mooly Sagiv and Sharon Shoham and James R. Wilcox and Doug Woos}, title = {Modularity for Decidability of Deductive Verification with Applications to Distributed Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {749-748}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

Program Analysis

Active Learning of Points-To Specifications
Osbert Bastani, Rahul Sharma, Alex Aiken, and Percy Liang
(Stanford University, USA; Microsoft Research, India)


@InProceedings{PLDI18p766, author = {Osbert Bastani and Rahul Sharma and Alex Aiken and Percy Liang}, title = {Active Learning of Points-To Specifications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {766-765}, doi = {}, year = {2018}, }

Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code
Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, and Charles Zhang
(Hong Kong University of Science and Technology, China; Sourcebrella, China)


@InProceedings{PLDI18p783, author = {Qingkai Shi and Xiao Xiao and Rongxin Wu and Jinguo Zhou and Gang Fan and Charles Zhang}, title = {Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {783-782}, doi = {}, year = {2018}, } Artifacts Functional

A Data-Driven CHC Solver
He Zhu, Stephen Magill, and Suresh Jagannathan
(Galois, USA; Purdue University, USA)


@InProceedings{PLDI18p800, author = {He Zhu and Stephen Magill and Suresh Jagannathan}, title = {A Data-Driven CHC Solver}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {800-799}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

User-Guided Program Reasoning using Bayesian Inference
Mukund Raghothaman, Sulekha Kulkarni, Kihong Heo, and Mayur Naik
(University of Pennsylvania, USA)


@InProceedings{PLDI18p817, author = {Mukund Raghothaman and Sulekha Kulkarni and Kihong Heo and Mayur Naik}, title = {User-Guided Program Reasoning using Bayesian Inference}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {817-816}, doi = {}, year = {2018}, } Artifacts Functional

Parallelism

GPU Code Optimization using Abstract Kernel Emulation and Sensitivity Analysis
Changwan Hong, Aravind Sukumaran-Rajam, Jinsung Kim, Prashant Singh Rawat, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, and P. Sadayappan
(Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA; Grenoble Alpes University, France; Inria, France)


@InProceedings{PLDI18p834, author = {Changwan Hong and Aravind Sukumaran-Rajam and Jinsung Kim and Prashant Singh Rawat and Sriram Krishnamoorthy and Louis-Noël Pouchet and Fabrice Rastello and P. Sadayappan}, title = {GPU Code Optimization using Abstract Kernel Emulation and Sensitivity Analysis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {834-833}, doi = {}, year = {2018}, }

Gluon: A Communication-Optimizing Substrate for Distributed Heterogeneous Graph Analytics
Roshan Dathathri, Gurbinder Gill, Loc Hoang, Hoang-Vu Dang, Alex Brooks, Nikoli Dryden, Marc Snir, and Keshav Pingali
(University of Texas at Austin, USA; University of Illinois at Urbana-Champaign, USA)


@InProceedings{PLDI18p851, author = {Roshan Dathathri and Gurbinder Gill and Loc Hoang and Hoang-Vu Dang and Alex Brooks and Nikoli Dryden and Marc Snir and Keshav Pingali}, title = {Gluon: A Communication-Optimizing Substrate for Distributed Heterogeneous Graph Analytics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {851-850}, doi = {}, year = {2018}, }

Heartbeat Scheduling: Provable Efficiency for Nested Parallelism
Umut A. Acar, Arthur Charguéraud, Adrien Guatto, Mike Rainey, and Filip Sieczkowski
(Carnegie Mellon University, USA; University of Strasbourg, France; Inria, France; CREST, USA)


@InProceedings{PLDI18p868, author = {Umut A. Acar and Arthur Charguéraud and Adrien Guatto and Mike Rainey and Filip Sieczkowski}, title = {Heartbeat Scheduling: Provable Efficiency for Nested Parallelism}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {868-867}, doi = {}, year = {2018}, }

Types

Guarded Impredicative Polymorphism
Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones
(Utrecht University, Netherlands; Microsoft Research, UK)


@InProceedings{PLDI18p885, author = {Alejandro Serrano and Jurriaan Hage and Dimitrios Vytiniotis and Simon Peyton Jones}, title = {Guarded Impredicative Polymorphism}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {885-884}, doi = {}, year = {2018}, }

Typed Closure Conversion for the Calculus of Constructions
William J. Bowman and Amal Ahmed
(Northeastern University, USA)


@InProceedings{PLDI18p902, author = {William J. Bowman and Amal Ahmed}, title = {Typed Closure Conversion for the Calculus of Constructions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {902-901}, doi = {}, year = {2018}, }

Inferring Type Rules for Syntactic Sugar
Justin Pombrio and Shriram Krishnamurthi
(Brown University, USA)


@InProceedings{PLDI18p919, author = {Justin Pombrio and Shriram Krishnamurthi}, title = {Inferring Type Rules for Syntactic Sugar}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {919-918}, doi = {}, year = {2018}, } Published Artifact Artifacts Available Artifacts Functional

proc time: 0.85