Venues / PLDI /

PLDI 2019

76 papers

A complete formal semantics of x86-64 user-level instruction set architecture · Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, Grigore Rosu
A fast analytical model of fully associative caches · Tobias Gysi, Tobias Grosser, Laurin Brandner, Torsten Hoefler
A typed, algebraic approach to parsing · Neelakantan R. Krishnaswami, Jeremy Yallop
Abstract interpretation under speculative execution · Meng Wu, Chao Wang
Accelerating sequential consistency for Java with speculative compilation · Lun Liu, Todd D. Millstein, Madanlal Musuvathi
An applied quantum Hoare logic · Li Zhou, Nengkun Yu, Mingsheng Ying
An inductive synthesis framework for verifiable reinforcement learning · He Zhu, Zikang Xiong, Stephen Magill, Suresh Jagannathan
Argosy: verifying layered storage systems with recovery refinement · Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
AutoPersist: an easy-to-use Java NVM framework based on reachability · Thomas Shull, Jian Huang, Josep Torrellas
Bidirectional type checking for relational properties · Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg
CHET: an optimizing compiler for fully-homomorphic neural-network inferencing · Roshan Dathathri, Olli Saarikivi, Hao Chen, Kim Laine, Kristin E. Lauter, Saeed Maleki + 2 more
Characterising renaming within OCaml's module system: theory and implementation · Reuben N. S. Rowe, Hugo Férée, Simon J. Thompson, Scott Owens
Co-optimizing memory-level parallelism and cache-level parallelism · Xulong Tang, Mahmut Taylan Kandemir, Mustafa Karaköy, Meenakshi Arunachalam
Compiling KB-sized machine learning models to tiny IoT devices · Sridhar Gopinath, Nikhil Ghanathe, Vivek Seshadri, Rahul Sharma
Composable, sound transformations of nested recursion and loops · Kirshanthan Sundararajah, Milind Kulkarni
Computing summaries of string loops in C for better testing and refactoring · Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Cristian Cadar
Continuously reasoning about programs using differential Bayesian inference · Kihong Heo, Mukund Raghothaman, Xujie Si, Mayur Naik
Cost analysis of nondeterministic probabilistic programs · Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, Wenjun Shi
DFix: automatically fixing timing bugs in distributed systems · Guangpu Li, Haopeng Liu, Xianglan Chen, Haryadi S. Gunawi, Shan Lu
Data-trace types for distributed stream processing systems · Konstantinos Mamouras, Caleb Stanford, Rajeev Alur, Zachary G. Ives, Val Tannen
Effective floating-point analysis via weak-distance minimization · Zhoulai Fu, Zhendong Su
FaCT: a DSL for timing-sensitive computation · Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner + 4 more
Gen: a general-purpose probabilistic programming system with programmable inference · Marco F. Cusumano-Towner, Feras A. Saad, Alexander K. Lew, Vikash K. Mansinghka
Generating piecewise-regular code from irregular structures · Travis Augustine, Janarthanan Sarma, Louis-Noël Pouchet, Gabriel Rodríguez
Genie: a generator of natural language semantic parsers for virtual assistant commands · Giovanni Campagna, Silei Xu, Mehrad Moradshahi, Richard Socher, Monica S. Lam
Huron: hybrid false sharing detection and repair · Tanvir Ahmed Khan, Yifan Zhao, Gilles Pokam, Barzan Mozafari, Baris Kasikci
ILC: a calculus for composable, computational cryptography · Kevin Liao, Matthew A. Hammer, Andrew Miller
Ignis: scaling distribution-oblivious systems with light-touch distribution · Nikos Vasilakis, Ben Karel, Yash Palkhiwala, John Sonchack, André DeHon, Jonathan M. Smith
Incremental precision-preserving symbolic inference for probabilistic programs · Jieyuan Zhang, Jingling Xue
Lazy counterfactual symbolic execution · William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, Ruzica Piskac
Learning stateful preconditions modulo a test generator · Angello Astorga, P. Madhusudan, Shambwaditya Saha, Shiyu Wang, Tao Xie
Lightweight multi-language syntax transformation with parser parser combinators · Rijnard van Tonder, Claire Le Goues
LoCal: a language for programs operating on serialized data · Michael Vollmer, Chaitanya Koparkar, Mike Rainey, Laith Sakka, Milind Kulkarni, Ryan R. Newton
Low-latency graph streaming using compressed purely-functional trees · Laxman Dhulipala, Guy E. Blelloch, Julian Shun
Mesh: compacting memory management for C/C++ applications · Bobby Powers, David Tench, Emery D. Berger, Andrew McGregor
Model checking for weakly consistent libraries · Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis
Model-driven transformations for multi- and many-core CPUs · Martin Kong, Louis-Noël Pouchet
Modular divide-and-conquer parallelization of nested loops · Azadeh Farzan, Victor Nicolet
Optimization and abstraction: a synergistic approach for analyzing neural network robustness · Greg Anderson, Shankara Pailoor, Isil Dillig, Swarat Chaudhuri
Panthera: holistic memory management for big data processing over hybrid memories · Chenxi Wang, Huimin Cui, Ting Cao, John N. Zigman, Haris Volos, Onur Mutlu + 3 more
Parallelism-centric what-if and differential analyses · Adarsh Yoga, Santosh Nagarakatte
Parser-directed fuzzing · Björn Mathis, Rahul Gopinath, Michaël Mera, Alexander Kampmann, Matthias Höschele, Andreas Zeller
Programming support for autonomizing software · Wen-Chuan Lee, Peng Liu, Yingqi Liu, Shiqing Ma, Xiangyu Zhang
Promising-ARM/RISC-V: a simpler and faster operational concurrency model · Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur
Proving differential privacy with shadow execution · Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, Danfeng Zhang
Renaissance: benchmarking suite for parallel applications on the JVM · Aleksandar Prokopec, Andrea Rosà, David Leopoldseder, Gilles Duboscq, Petr Tuma, Martin Studener + 6 more
Replication-aware linearizability · Chao Wang, Constantin Enea, Suha Orhun Mutluergil, Gustavo Petri
Resource-guided program synthesis · Tristan Knoth, Di Wang, Nadia Polikarpova, Jan Hoffmann
Reusable inline caching for JavaScript performance · Jiho Choi, Thomas Shull, Josep Torrellas
Robustness against release/acquire semantics · Ori Lahav, Roy David Margalit
SLING: using dynamic analysis to infer program invariants in separation logic · Ton Chanh Le, Guolong Zheng, ThanhVu Nguyen
Scalable taint specification inference with big code · Victor Chibotaru, Benjamin Bichsel, Veselin Raychev, Martin T. Vechev
Scalable verification of probabilistic networks · Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen + 1 more
Scenic: a language for scenario specification and scene generation · Daniel J. Fremont, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
SemCluster: clustering of imperative programming assignments based on quantitative semantic features · David Mitchel Perry, Dohyeong Kim, Roopsha Samanta, Xiangyu Zhang
Semantic program alignment for equivalence checking · Berkeley R. Churchill, Oded Padon, Rahul Sharma, Alex Aiken
Simple and precise static analysis of untrusted Linux kernel extensions · Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky + 2 more
Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs · Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn
Sound regular expression semantics for dynamic symbolic execution of JavaScript · Blake Loring, Duncan Mitchell, Johannes Kinder
Sound, fine-grained traversal fusion for heterogeneous trees · Laith Sakka, Kirshanthan Sundararajah, Ryan R. Newton, Milind Kulkarni
Sparse computation data dependence simplification for efficient compiler-generated inspectors · Mahdi Soltan Mohammadi, Tomofumi Yuki, Kazem Cheshmi, Eddie C. Davis, Mary W. Hall, Maryam Mehri Dehnavi + 4 more
Sparse record and replay with controlled scheduling · Christopher Lidbury, Alastair F. Donaldson
Supporting peripherals in intermittent systems with just-in-time checkpoints · Kiwan Maeng, Brandon Lucia
Synthesis and machine learning for heterogeneous extraction · Arun Iyer, Manohar Jonnalagedda, Suresh Parthasarathy, Arjun Radhakrishna, Sriram K. Rajamani
Synthesizing database programs for schema refactoring · Yuepeng Wang, James Dong, Rushi Shah, Isil Dillig
Toward efficient gradual typing for structural types via coercions · Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, Jeremy G. Siek
Towards certified separate compilation for concurrent programs · Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, Xinyu Feng
Transactional concurrency control for intermittent, energy-harvesting computing systems · Emily Ruppel, Brandon Lucia
Type-level computations for Ruby libraries · Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn
Unsupervised learning of API aliasing specifications · Jan Eberhardt, Samuel Steffen, Veselin Raychev, Martin T. Vechev
Using active learning to synthesize models of applications that access databases · Jiasi Shen, Martin C. Rinard
Usuba: high-throughput and constant-time ciphers, by construction · Darius Mercadier, Pierre-Évariste Dagand
Verification of programs under the release-acquire semantics · Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, Shankara Narayanan Krishna
Verified compilation on a verified processor · Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson + 1 more
Verifying message-passing programs with dependent behavioural types · Alceste Scalas, Nobuko Yoshida, Elias Benussi
Wootz: a compiler-based framework for fast CNN pruning via composability · Hui Guan, Xipeng Shen, Seung-Hwan Lim