| 2013 | A Data Driven Approach for Algebraic Loop Invariants. Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, Aditya V. Nori |
| 2013 | A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness. Ioannis T. Kassios, Eleftherios Kritikos |
| 2013 | Abstract Refinement Types. Niki Vazou, Patrick Maxim Rondon, Ranjit Jhala |
| 2013 | Automatic Type Inference for Amortised Heap-Space Analysis. Martin Hofmann, Dulma Rodriguez |
| 2013 | Behavioral Polymorphism and Parametricity in Session-Based Communication. Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho |
| 2013 | Checking and Enforcing Robustness against TSO. Ahmed Bouajjani, Egor Derevenetc, Roland Meyer |
| 2013 | Compositional Invariant Checking for Overlaid and Nested Linked Lists. Constantin Enea, Vlad Saveluc, Mihaela Sighireanu |
| 2013 | Concurrent Flexible Reversibility. Ivan Lanese, Michael Lienhardt, Claudio Antares Mezzina, Alan Schmitt, Jean-Bernard Stefani |
| 2013 | Constraining Delimited Control with Contracts. Asumu Takikawa, T. Stephen Strickland, Sam Tobin-Hochstadt |
| 2013 | Counterexample-Guided Precondition Inference. Mohamed Nassim Seghir, Daniel Kroening |
| 2013 | Distributed Electronic Rights in JavaScript. Mark S. Miller, Tom Van Cutsem, Bill Tulloh |
| 2013 | FliPpr: A Prettier Invertible Printing System. Kazutaka Matsuda, Meng Wang |
| 2013 | GADTs Meet Subtyping. Gabriel Scherer, Didier Rémy |
| 2013 | Higher-Order Processes, Functions, and Sessions: A Monadic Integration. Bernardo Toninho, Luís Caires, Frank Pfenning |
| 2013 | Information Reuse for Multi-goal Reachability Analyses. Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith |
| 2013 | Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels. Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer |
| 2013 | Language Constructs for Non-Well-Founded Computation. Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva |
| 2013 | Laziness by Need. Stephen Chang |
| 2013 | Model-Checking Higher-Order Programs with Recursive Types. Naoki Kobayashi, Atsushi Igarashi |
| 2013 | Modular Reasoning about Separation of Concurrent Data Structures. Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson |
| 2013 | On Distributability in Process Calculi. Kirstin Peters, Uwe Nestmann, Ursula Goltz |
| 2013 | Pretty-Big-Step Semantics. Arthur Charguéraud |
| 2013 | Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings Matthias Felleisen, Philippa Gardner |
| 2013 | Quarantining Weakness - Compositional Reasoning under Relaxed Memory Models (Extended Abstract). Radha Jagadeesan, Gustavo Petri, Corin Pitcher, James Riely |
| 2013 | Ribbon Proofs for Separation Logic. John Wickerson, Mike Dodds, Matthew J. Parkinson |
| 2013 | Slicing-Based Trace Analysis of Rewriting Logic Specifications with iJulienne. María Alpuente, Demis Ballis, Francisco Frechina, Julia Sapiña |
| 2013 | Software Verification for Weak Memory via Program Transformation. Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig |
| 2013 | Structural Lock Correlation with Ownership Types. Yi Lu, John Potter, Jingling Xue |
| 2013 | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems. Joost-Pieter Katoen, Doron A. Peled |
| 2013 | The Compiler Forest. Mihai Budiu, Joel Galenson, Gordon D. Plotkin |
| 2013 | Verifying Concurrent Memory Reclamation Algorithms with Grace. Alexey Gotsman, Noam Rinetzky, Hongseok Yang |
| 2013 | Verifying Concurrent Programs against Sequential Specifications. Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza |
| 2013 | Why3 - Where Programs Meet Provers. Jean-Christophe Filliâtre, Andrei Paskevich |