Venues / PLDI /

PLDI 2020

77 papers

A marriage of pointer- and epoch-based reclamation · Jeehoon Kang, Jaehwang Jung
A study of the learnability of relational properties: model counting meets machine learning (MCML) · Muhammad Usman, Wenxi Wang, Marko Vasic, Kaiyuan Wang, Haris Vikalo, Sarfraz Khurshid
Adaptive low-overhead scheduling for periodic and reactive intermittent execution · Kiwan Maeng, Brandon Lucia
Armada: low-effort verification of high-performance concurrent programs · Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma + 2 more
Automated derivation of parametric data movement lower bounds for affine programs · Auguste Olivry, Julien Langou, Louis-Noël Pouchet, P. Sadayappan, Fabrice Rastello
Automatic generation of efficient sparse tensor format conversion routines · Stephen Chou, Fredrik Kjolstad, Saman P. Amarasinghe
Behavioral simulation for smart contracts · Sidi Mohamed Beillahi, Gabriela F. Ciocarlie, Michael Emmi, Constantin Enea
Binary rewriting without control flow recovery · Gregory J. Duck, Xiang Gao, Abhik Roychoudhury
BlankIt library debloating: getting what you want instead of cutting what you don't · Chris Porter, Girish Mururu, Prithayan Barua, Santosh Pande
Blended, precise semantic program embeddings · Ke Wang, Zhendong Su
CARAT: a case for virtual memory through compiler- and runtime-based address translation · Brian Suchy, Simone Campanoni, Nikos Hardavellas, Peter A. Dinda
CacheQuery: learning replacement policies from hardware caches · Pepe Vila, Pierre Ganty, Marco Guarnieri, Boris Köpf
Compiler and runtime support for continuation marks · Matthew Flatt, R. Kent Dybvig
Compiler-directed soft error resilience for lightweight GPU register file protection · Hongjune Kim, Jianping Zeng, Qingrui Liu, Mohammad Abdel-Majeed, Jaejin Lee, Changhee Jung
Constant-time foundations for the new spectre era · Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk + 1 more
Crafty: efficient, HTM-compatible persistent transactions · Kaan Genç, Michael D. Bond, Guoqing Harry Xu
Data-driven inference of representation invariants · Anders Miltner, Saswat Padhi, Todd D. Millstein, David Walker
Debug information validation for optimized code · Yuanbo Li, Shuo Ding, Qirun Zhang, Davide Italiano
Debugging and detecting numerical errors in computation with posits · Sangeeta Chowdhary, Jay P. Lim, Santosh Nagarakatte
Decidable verification under a causally consistent shared memory · Ori Lahav, Udi Boker
Detecting network load violations for distributed control planes · Kausik Subramanian, Anubhavnidhi Abhashkumar, Loris D'Antoni, Aditya Akella
EVA: an encrypted vector arithmetic language and compiler for efficient homomorphic computation · Roshan Dathathri, Blagovesta Kostova, Olli Saarikivi, Wei Dai, Kim Laine, Madan Musuvathi
Effective function merging in the SSA form · Rodrigo C. O. Rocha, Pavlos Petoumenos, Zheng Wang, Murray Cole, Hugh Leather
Efficient handling of string-number conversion · Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Petr Janku + 3 more
Ethainter: a smart contract security analyzer for composite vulnerabilities · Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, Yannis Smaragdakis
Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems · Qinheping Hu, John Cyphert, Loris D'Antoni, Thomas W. Reps
Fast graph simplification for interleaved Dyck-reachability · Yuanbo Li, Qirun Zhang, Thomas W. Reps
Faster general parsing through context-free memoization · Grzegorz Herman
First-order quantified separators · Jason R. Koenig, Oded Padon, Neil Immerman, Alex Aiken
FreezeML: complete and easy type inference for first-class polymorphism · Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, Jonathan Coates
From folklore to fact: comparing implementations of stacks and continuations · Kavon Farvardin, John H. Reppy
Gillian, part i: a multi-language platform for symbolic execution · José Fragoso Santos, Petar Maksimovic, Sacha-Élie Ayoun, Philippa Gardner
HipHop.js: (A)Synchronous reactive web programming · Gérard Berry, Manuel Serrano
Improving program locality in the GC using hotness · Albert Mingkun Yang, Erik Österlund, Tobias Wrigstad
Inductive sequentialization of asynchronous programs · Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, Shaz Qadeer
LLHD: a multi-level intermediate representation for hardware description languages · Fabian Schuiki, Andreas Kurth, Tobias Grosser, Luca Benini
Learning fast and precise numerical analysis · Jingxuan He, Gagandeep Singh, Markus Püschel, Martin T. Vechev
Learning nonlinear loop invariants with gated continuous logic networks · Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, Ronghui Gu
Multi-modal synthesis of regular expressions · Qiaochu Chen, Xinyu Wang, Xi Ye, Greg Durrett, Isil Dillig
NV: an intermediate language for verification of network control planes · Nick Giannarakis, Devon Loehr, Ryan Beckett, David Walker
NVTraverse: in NVRAM data structures, the destination is more important than the journey · Michal Friedman, Naama Ben-David, Yuanhao Wei, Guy E. Blelloch, Erez Petrank
OOElala: order-of-evaluation based alias analysis for compiler optimization · Ankush Phulia, Vaibhav Bhagee, Sorav Bansal
On the principles of differentiable quantum programming languages · Shaopeng Zhu, Shih-Han Hung, Shouvanik Chakrabarti, Xiaodi Wu
Optimizing homomorphic evaluation circuits by program synthesis and term rewriting · DongKwon Lee, Woosuk Lee, Hakjoo Oh, Kwangkeun Yi
PMEvo: portable inference of port mappings for out-of-order processors by evolutionary optimization · Fabian Ritter, Sebastian Hack
PMThreads: persistent memory threads harnessing versioned shadow copies · Zhenwei Wu, Kai Lu, Andrew Nisbet, Wenzhe Zhang, Mikel Luján
Polynomial invariant generation for non-deterministic recursive programs · Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady
Predictable accelerator design with time-sensitive affine types · Rachit Nigam, Sachille Atapattu, Samuel Thomas, Zhijing Li, Theodore Bauer, Yuwei Ye + 3 more
Promising 2.0: global optimizations in relaxed memory concurrency · Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav + 1 more
Proving almost-sure termination by omega-regular decomposition · Jianhui Chen, Fei He
Proving data-poisoning robustness in decision trees · Samuel Drews, Aws Albarghouthi, Loris D'Antoni
Question selection for interactive program synthesis · Ruyi Ji, Jingjing Liang, Yingfei Xiong, Lu Zhang, Zhenjiang Hu
Reactive probabilistic programming · Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, Michael Carbin
Reconciling enumerative and deductive program synthesis · Kangjing Huang, Xiaokang Qiu, Peiyuan Shen, Yanjun Wang
Repairing and mechanising the JavaScript relaxed memory model · Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur + 2 more
Responsive parallelism with futures and state · Stefan K. Muller, Kyle Singer, Noah Goldstein, Umut A. Acar, Kunal Agrawal, I-Ting Angelina Lee
SCAF: a speculation-aware collaborative dependence analysis framework · Sotiris Apostolakis, Ziyang Xu, Zujun Tan, Greg Chan, Simone Campanoni, David I. August
Scalable validation of binary lifters · Sandeep Dasgupta, Sushant Dinesh, Deepan Venkatesh, Vikram S. Adve, Christopher W. Fletcher
Securing smart contract with runtime validation · Ao Li, Jemin Andrew Choi, Fan Long
Semantic code search via equational reasoning · Varot Premtoon, James Koppel, Armando Solar-Lezama
Silq: a high-level quantum language with safe uncomputation and intuitive semantics · Benjamin Bichsel, Maximilian Baader, Timon Gehr, Martin T. Vechev
SmartTrack: efficient predictive race detection · Jake Roemer, Kaan Genç, Michael D. Bond
Static analysis of Java enterprise applications: frameworks and caches, the elephants in the room · Anastasios Antoniadis, Nikos Filippakis, Paddy Krishnan, Raghavendra Ramesh, Nicholas Allen, Yannis Smaragdakis
SympleGraph: distributed graph processing with precise loop-carried dependency guarantee · Youwei Zhuo, Jingji Chen, Qinyi Luo, Yanzhi Wang, Hailong Yang, Depei Qian + 1 more
Synthesizing structured CAD models with equality saturation and inverse transformations · Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman + 1 more
Templates and recurrences: better together · Jason Breck, John Cyphert, Zachary Kincaid, Thomas W. Reps
The essence of Bluespec: a core language for rule-based hardware design · Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind
Towards a verified range analysis for JavaScript JITs · Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, Deian Stefan
Towards an API for the real numbers · Hans-Juergen Boehm
Type error feedback via analytic program repair · Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, Ranjit Jhala
Type-directed scheduling of streaming accelerators · David Durst, Matthew Feldman, Dillon Huff, David Akeley, Ross G. Daly, Gilbert Louis Bernstein + 3 more
Typilus: neural type hints · Miltiadis Allamanis, Earl T. Barr, Soline Ducousso, Zheng Gao
Understanding memory and thread safety practices and issues in real-world Rust programs · Boqin Qin, Yilun Chen, Zeming Yu, Linhai Song, Yiying Zhang
Validating SMT solvers via semantic fusion · Dominik Winterer, Chengyu Zhang, Zhendong Su
Verifying concurrent search structure templates · Siddharth Krishna, Nisarg Patel, Dennis E. Shasha, Thomas Wies
Zippy LL(1) parsing with derivatives · Romain Edelmann, Jad Hamza, Viktor Kuncak
λPSI: exact inference for higher-order probabilistic programs · Timon Gehr, Samuel Steffen, Martin T. Vechev