List of accepted papers

• Points-To Analysis with Efficient Strong Updates: O. Lhotak, K. Chung
• Pick Your Contexts Well: Understanding Object-Sensitivity (The Making of a Precise and Scalable Pointer Analysis): Y. Smaragdakis, M. Bravenboer, O. Lhotak
• Multivariate Amortized Resource Analysis: J. Hoffmann, K. Aehlig, M. Hofmann
• Making Prophecies with Decision Predicates: B. Cook, E. Koskinen
• Space Overhead Bounds for Dynamic Memory Management with Partial Compaction: A. Bendersky, E. Petrank
• Precise Reasoning for Programs Using Containers: I. Dillig, T. Dillig, A. Aiken
• The Essence of Compiling with Traces: S. Guo, J. Palsberg
• Geometry of Synthesis III: Resource management through type inference: D. Ghica, A. Smith
• A separation logic for refining concurrent objects: A. Turon, M. Wand
• A Shape Analysis for Optimizing Parallel Graph Programs: D. Prountzos, R. Manevich, K. Pingali, K. McKinley
• A typed store-passing translation for general references: F. Pottier
• Resourceable, Retargetable, Modular Instruction Selection Using a Machine-Independent, Type-Based Tiling of Low-Level Intermediate Code, N. Ramsey, J. Dias
• Relaxed-Memory Concurrency and Verified Compilation: J. Sevcik, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, P. Sewell
• Mathematizing C++ Concurrency: M. Batty, S. Owens, S. Sarkar, P. Sewell, T. Weber
• A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis: P. Cousot, R. Cousot, F. Logozzo
• EigenCFA Accelerating flow analysis with GPUs: T. Prabhu, S. Ramalingam, M. Might, M. Ha
• Bisimulation for quantum processes: Y. Feng, R. Duan, M. Ying
• Formal verification of object layout for C++ multiple inheritance: T. Ramananandro, G. Reis, X. Leroy
• Blame for All: A. Ahmed, R. Findler, J. Siek, P. Wadler
• Step-Indexed Kripke Models over Recursive Worlds: L. Birkedal, B. Reus, J. Schwinghammer, K. Stovring, J. Thamsborg, H. Yang
• Static Analysis for Multi-Staged Programs via Unstaging Translation: W. Choi, B. Aktemur, K. Yi, M. Tatsuta
• Modular Reasoning for Deterministic Parallelism: M. Dodds, S. Jagannathan, M. Parkinson
• Fresh-Register Automata: N. Tzevelekos
• Streaming transducers for algorithmic verification of single-pass list-processing programs: R. Alur, P. Cerny
• The Tree Width of Auxiliary Storage: P. Madhusudan, G. Parlato
• Loop Transformations: Convexity, Pruning and Optimization: L. Pouchet, U. Bondhugula, C. Bastoul, A. Cohen, J. Ramanujam, P. Sadayappan, N. Vasilache
• Static analysis of interrupt-driven programs: M. Schwarz, H. Seidl, V. Vojdani, M. Müller-Olm, P. Lammich
• Expressive Modular Fine-Grained Concurrency Specification: B. Jacobs, F. Piessens
• Generative type abstraction and type-level computation: S. Weirich, D. Vytiniotis, S. Peyton-Jones, S. Zdancewic
• A Kripke Logical Relation Between ML and Assembly: C. Hur, D. Dreyer
• Laws of Order: Expensive Synchronization in Concurrent Algorithms Cannot be Eliminated: H. Attiya, R. Guerraoui, D. Hendler, P. Kuznetsov, M. Michael, M. Vechev
• On Interference Abstractions: N. Sinha, C. Wang
• Decidable logics combining heap structures and data: P. Madhusudan, G. Parlato, X. Qiu
• Correct Blame for Contracts: No More Scapegoating: C. Dimoulas, R. Findler, C. Flanagan, M. Felleisen
• Safe Nondeterminism in a Deterministic-by-Default Parallel Language: R. Bocchino, S. Heumann, N. Honarmand, S. Adve, V. Adve, A. Welc, T. Shpeisman
• Dynamic Multirole Session Types: P. Deniélou, N. Yoshida
• Calling Context Abstraction with Shapes: X. Rival, B. Chang
• Delay-bounded scheduling:  M. Emmi, S. Qadeer, Z. Rakamaric
• Vector Addition System Reachability Problem In Less Than 7 Pages: J. Leroux
• Automating String Processing in Spreadsheets using Input-Output Examples. S. Gulwani
• Constraint Based Inference of Auxiliary Variables and Relies/Guarantees for Verifying Multi-Threaded Programs: A. Gupta, C. Popeea, A. Rybalchenko
• Complexity of Pattern-based Verification for Multithreaded Programs: J. Esparza, P. Ganty
• Elements of Symmetric Lenses:  M. Hofmann, B. Pierce, D. Wagner
• Dynamic Inference of Static Types for Ruby: J. An, A. Chaudhuri, J. Foster, M. Hicks
• Verifying Higher-Order Programs with Pattern-Matching Algebraic Data Types. C. Ong, S. Ramsay
• Learning Minimal Abstractions: P. Liang, O. Tripp, M. Naik
• Practical Affine Types: J. Tov, R. Pucella
• A Technique for the Effective and Automatic Reuse of Classical Compiler Optimizations on Multithreaded Code:Pramod G. Joisha, Robert S. Schreiber, Prithviraj Banerjee, Hans-J. Boehm, Dhruva R. Chakrabarti
• Regular Expression Containment: Coinductive Axiomatization and Computational Interpretation: Fritz Henglein, Lasse Nielsen