Venues / PLDI /

PLDI 2016

48 papers

A design and verification methodology for secure isolated regions · Rohit Sinha, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram K. Rajamani, Sanjit A. Seshia + 1 more
A distributed OpenCL framework using redundant computation and data replication · Junghyun Kim, Gangwon Jo, Jaehoon Jung, Jungwon Kim, Jaejin Lee
Accepting blame for safe tunneled exceptions · Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, Andrew C. Myers
Assessing the limits of program-specific garbage collection performance · Nicholas Jacek, Meng-Chieh Chiu, Benjamin M. Marlin, Eliot Moss
Automatically learning shape specifications · He Zhu, Gustavo Petri, Suresh Jagannathan
Cardinalities and universal quantifiers for verifying parameterized systems · Klaus von Gleissenthall, Nikolaj S. Bjørner, Andrey Rybalchenko
Cartesian hoare logic for verifying k-safety properties · Marcelo Sousa, Isil Dillig
Configuration synthesis for programmable analog devices with Arco · Sara Achour, Rahul Sarpeshkar, Martin C. Rinard
Coverage-directed differential testing of JVM implementations · Yuting Chen, Ting Su, Chengnian Sun, Zhendong Su, Jianjun Zhao
Data-driven precondition inference with learned features · Saswat Padhi, Rahul Sharma, Todd D. Millstein
Effective padding of multidimensional arrays to avoid cache conflict misses · Changwan Hong, Wenlei Bao, Albert Cohen, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello + 2 more
End-to-end verification of information-flow security for C and assembly programs · David Costanzo, Zhong Shao, Ronghui Gu
Event-driven network programming · Jedidiah McClurg, Hossein Hojjat, Nate Foster, Pavol Cerný
Exposing errors related to weak memory in GPU applications · Tyler Sorensen, Alastair F. Donaldson
Fast synthesis of fast collections · Calvin Loncaric, Emina Torlak, Michael D. Ernst
FlexVec: auto-vectorization for irregular loops · Sara S. Baghsorkhi, Nalini Vasudevan, Youfeng Wu
From Datalog to flix: a declarative language for fixed points on lattices · Magnus Madsen, Ming-Ho Yee, Ondrej Lhoták
GreenWeb: language extensions for energy-efficient mobile web computing · Yuhao Zhu, Vijay Janapa Reddi
Higher-order and tuple-based massively-parallel prefix sums · Sepideh Maleki, Annie Yang, Martin Burtscher
Idle time garbage collection scheduling · Ulan Degenbaev, Jochen Eisinger, Manfred Ernst, Ross McIlroy, Hannes Payer
Input responsiveness: using canary inputs to dynamically steer approximation · Michael A. Laurenzano, Parker Hill, Mehrzad Samadi, Scott A. Mahlke, Jason Mars, Lingjia Tang
Into the depths of C: elaborating the de facto standards · Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson + 1 more
Ivy: safety verification by interactive generalization · Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham
Just-in-time static type checking for dynamic languages · Brianna M. Ren, Jeffrey S. Foster
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 + 1 more
Lightweight computation tree tracing for lazy functional languages · Maarten Faddegon, Olaf Chitil
Living on the edge: rapid-toggling probes with cross-modification on x86 · Buddhika Chamith, Bo Joel Svensson, Luke Dalessandro, Ryan R. Newton
MapReduce program synthesis · Calvin Smith, Aws Albarghouthi
Occurrence typing modulo theories · Andrew M. Kent, David Kempe, Sam Tobin-Hochstadt
On the complexity and performance of parsing with derivatives · Michael D. Adams, Celeste Hollenbeck, Matthew Might
Polymorphic type inference for machine code · Matthew Noonan, Alexey Loginov, David R. Cok
Precise, dynamic information flow for database-backed applications · Jean Yang, Travis Hance, Thomas H. Austin, Armando Solar-Lezama, Cormac Flanagan, Stephen Chong
Program synthesis from polymorphic refinement types · Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama
Programmatic and direct manipulation, together at last · Ravi Chugh, Brian Hempel, Mitchell Spradlin, Jacob Albers
Refinement types for TypeScript · Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
Rehearsal: a configuration verification tool for puppet · Rian Shambaugh, Aaron Weiss, Arjun Guha
Remix: online detection and repair of cache contention for the JVM · Ariel Eizenberg, Shiliang Hu, Gilles Pokam, Joseph Devietti
SDNRacer: concurrency analysis for software-defined networks · Ahmed El-Hassany, Jeremie Miserez, Pavol Bielik, Laurent Vanbever, Martin T. Vechev
Statistical similarity of binaries · Yaniv David, Nimrod Partush, Eran Yahav
Stratified synthesis: automatically learning the x86-64 instruction set · Stefan Heule, Eric Schkufza, Rahul Sharma, Alex Aiken
Synthesizing transformations on hierarchically structured data · Navid Yaghmazadeh, Christian Klinger, Isil Dillig, Swarat Chaudhuri
Temporal NetKAT · Ryan Beckett, Michael Greenberg, David Walker
Toward compositional verification of interruptible OS kernels and device drivers · Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu
Transactional data structure libraries · Alexander Spiegelman, Guy Golan-Gueta, Idit Keidar
Types from data: making structured data first-class citizens in F# · Tomas Petricek, Gustavo Guerra, Don Syme
Verified lifting of stencil computations · Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, Armando Solar-Lezama
Verified peephole optimizations for CompCert · Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman
Verifying bit-manipulations of floating-point · Wonyeol Lee, Rahul Sharma, Alex Aiken