Table of Contents

• Into the depths of C: elaborating the de facto standardsKayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, Peter Sewell. 1-15 [doi]
• Living on the edge: rapid-toggling probes with cross-modification on x86Buddhika Chamith, Bo Joel Svensson, Luke Dalessandro, Ryan R. Newton. 16-26 [doi]
• Polymorphic type inference for machine codeMatthew Noonan, Alexey Loginov, David Cok. 27-41 [doi]
• Data-driven precondition inference with learned featuresSaswat Padhi, Rahul Sharma, Todd D. Millstein. 42-56 [doi]
• Cartesian hoare logic for verifying k-safety propertiesMarcelo Sousa, Isil Dillig. 57-69 [doi]
• Verifying bit-manipulations of floating-pointWonyeol Lee, Rahul Sharma 0001, Alex Aiken. 70-84 [doi]
• Coverage-directed differential testing of JVM implementationsYuting Chen, Ting Su, Chengnian Sun, Zhendong Su, Jianjun Zhao. 85-99 [doi]
• Exposing errors related to weak memory in GPU applicationsTyler Sorensen, Alastair F. Donaldson. 100-113 [doi]
• Lightweight computation tree tracing for lazy functional languagesMaarten Faddegon, Olaf Chitil. 114-128 [doi]
• Effective padding of multidimensional arrays to avoid cache conflict missesChangwan Hong, Wenlei Bao, Albert Cohen 0001, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, J. Ramanujam, P. Sadayappan. 129-144 [doi]
• GreenWeb: language extensions for energy-efficient mobile web computingYuhao Zhu, Vijay Janapa Reddi. 145-160 [doi]
• Input responsiveness: using canary inputs to dynamically steer approximationMichael A. Laurenzano, Parker Hill, Mehrzad Samadi, Scott A. Mahlke, Jason Mars, Lingjia Tang. 161-176 [doi]
• Configuration synthesis for programmable analog devices with ArcoSara Achour, Rahul Sarpeshkar, Martin C. Rinard. 177-193 [doi]
• From Datalog to flix: a declarative language for fixed points on latticesMagnus Madsen, Ming-Ho Yee, Ondrej Lhoták. 194-208 [doi]
• Latte: a language, compiler, and runtime for elegant and efficient deep neural networksLeonard Truong, Rajkishore Barik, Ehsan Totoni, Hai Liu, Chick Markley, Armando Fox, Tatiana Shpeisman. 209-223 [doi]
• On the complexity and performance of parsing with derivativesMichael D. Adams, Celeste Hollenbeck, Matthew Might. 224-236 [doi]
• Stratified synthesis: automatically learning the x86-64 instruction setStefan Heule, Eric Schkufza, Rahul Sharma 0001, Alex Aiken. 237-250 [doi]
• Remix: online detection and repair of cache contention for the JVMAriel Eizenberg, Shiliang Hu, Gilles Pokam, Joseph Devietti. 251-265 [doi]
• Statistical similarity of binariesYaniv David, Nimrod Partush, Eran Yahav. 266-280 [doi]
• Accepting blame for safe tunneled exceptionsYizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, Andrew C. Myers. 281-295 [doi]
• Occurrence typing modulo theoriesAndrew M. Kent, David Kempe, Sam Tobin-Hochstadt. 296-309 [doi]
• Refinement types for TypeScriptPanagiotis Vekris, Benjamin Cosman, Ranjit Jhala. 310-325 [doi]
• MapReduce program synthesisCalvin Smith, Aws Albarghouthi. 326-340 [doi]
• Programmatic and direct manipulation, together at lastRavi Chugh, Brian Hempel, Mitchell Spradlin, Jacob Albers. 341-354 [doi]
• Fast synthesis of fast collectionsCalvin Loncaric, Emina Torlak, Michael D. Ernst. 355-368 [doi]
• Event-driven network programmingJedidiah McClurg, Hossein Hojjat, Nate Foster, Pavol Cerný. 369-385 [doi]
• Temporal NetKATRyan Beckett, Michael Greenberg, David Walker. 386-401 [doi]
• SDNRacer: concurrency analysis for software-defined networksAhmed El-Hassany, Jeremie Miserez, Pavol Bielik, Laurent Vanbever, Martin T. Vechev. 402-415 [doi]
• Rehearsal: a configuration verification tool for puppetRian Shambaugh, Aaron Weiss, Arjun Guha. 416-430 [doi]
• Toward compositional verification of interruptible OS kernels and device driversHao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu. 431-447 [doi]
• Verified peephole optimizations for CompCertEric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman. 448-461 [doi]
• Just-in-time static type checking for dynamic languagesBrianna M. Ren, Jeffrey S. Foster. 462-476 [doi]
• Types from data: making structured data first-class citizens in F#Tomas Petricek, Gustavo Guerra, Don Syme. 477-490 [doi]
• Automatically learning shape specificationsHe Zhu, Gustavo Petri, Suresh Jagannathan. 491-507 [doi]
• Synthesizing transformations on hierarchically structured dataNavid Yaghmazadeh, Christian Klinger, Isil Dillig, Swarat Chaudhuri. 508-521 [doi]
• Program synthesis from polymorphic refinement typesNadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama. 522-538 [doi]
• Higher-order and tuple-based massively-parallel prefix sumsSepideh Maleki, Annie Yang, Martin Burtscher. 539-552 [doi]
• A distributed OpenCL framework using redundant computation and data replicationJunghyun Kim, Gangwon Jo, Jaehoon Jung, Jungwon Kim, Jaejin Lee. 553-569 [doi]
• Idle time garbage collection schedulingUlan Degenbaev, Jochen Eisinger, Manfred Ernst, Ross McIlroy, Hannes Payer. 570-583 [doi]
• Assessing the limits of program-specific garbage collection performanceNicholas Jacek, Meng-Chieh Chiu, Benjamin M. Marlin, Eliot Moss. 584-598 [doi]
• Cardinalities and universal quantifiers for verifying parameterized systemsKlaus von Gleissenthall, Nikolaj Bjørner, Andrey Rybalchenko. 599-613 [doi]
• Ivy: safety verification by interactive generalizationOded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham. 614-630 [doi]
• Precise, dynamic information flow for database-backed applicationsJean Yang, Travis Hance, Thomas H. Austin, Armando Solar-Lezama, Cormac Flanagan, Stephen Chong. 631-647 [doi]
• End-to-end verification of information-flow security for C and assembly programsDavid Costanzo, Zhong Shao, Ronghui Gu. 648-664 [doi]
• A design and verification methodology for secure isolated regionsRohit Sinha 0001, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram K. Rajamani, Sanjit A. Seshia, Kapil Vaswani. 665-681 [doi]
• Transactional data structure librariesAlexander Spiegelman, Guy Golan-Gueta, Idit Keidar. 682-696 [doi]
• FlexVec: auto-vectorization for irregular loopsSara S. Baghsorkhi, Nalini Vasudevan, Youfeng Wu. 697-710 [doi]
• Verified lifting of stencil computationsShoaib Kamil, Alvin Cheung, Shachar Itzhaky, Armando Solar-Lezama. 711-726 [doi]