ESOP 2013: List of accepted and conditionally accepted papers
Proceedings: Springer Lecture Notes in Computer Science 7792
- Alexey Gotsman, Noam Rinetzky and Hongseok Yang. Verifying Concurrent Memory Reclamation Algorithms with Grace
- Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema and Shaz Qadeer. Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
- Radha Jagadeesan, Gustavo Petri, Corin Pitcher and James Riely. Quarantining Weakness: Compositional Reasoning Under Relaxed Memory Models
- Dirk Beyer, Andreas Holzer, Michael Tautschnig and Helmut Veith. Information Reuse for Multi-goal Reachability Analyses
- Yi Lu, John Potter and Jingling Xue. Structural Lock Correlation with Ownership Types
- Luis Caires, Jorge A. Pérez, Frank Pfenning and Bernardo Toninho. Behavioral Polymorphism and Parametricity in Session-Based Communication
- Niki Vazou, Patrick Rondon and Ranjit Jhala. Abstract Refinement Types
- Kirstin Peters, Uwe Nestmann and Ursula Goltz. On Distributability in Process Calculi
- Constantin Enea, Vlad Saveluc and Mihaela Sighireanu. Compositional Invariant Checking for Overlaid and Nested Linked Lists
- Ahmed Bouajjani, Egor Derevenetc and Roland Meyer. Robustness Checking against TSO
- Arthur Charguéraud. Pretty-Big-Step Semantics
- Ahmed Bouajjani, Michael Emmi, Constantin Enea and Jad Hamza. Verifying Concurrent Programs Against Sequential Specifications
- Asumu Takikawa, T. Stephen Strickland and Sam Tobin-Hochstadt. Constraining Delimited Control with Contracts
- Jade Alglave, Daniel Kroening, Vincent Nimal and Michael Tautschnig. Software Verification for Weak Memory via Program Transformation
- Mohamed Nassim Seghir and Daniel Kroening. Counterexample Guided Precondition Inference
- Kazutaka Matsuda and Meng Wang. FliPpr: A Prettier Invertible Printing System
- Bernardo Toninho, Luis Caires and Frank Pfenning. Higher-Order Processes, Functions, and Sessions: A Monadic Integration
- Naoki Kobayashi and Atsushi Igarashi. Model-Checking Higher-Order Programs with Recursive Types
- Kasper Svendsen, Lars Birkedal and Matthew Parkinson. Modular Reasoning about Separation of Concurrent Data Structures
- Stephen Chang. Laziness By Need
- Ioannis Kassios and Eleftherios Kritikos. A Discipline for Program Verification based on Backpointers and its Use in Observational Disjointness
- María Alpuente, Demis Ballis, Francisco Frechina and Julia Sapiña. Slicing-based Trace Analysis of Rewriting Logic Specifications with iJulienne
- Jean-Christophe Filliatre and Andrei Paskevich. Why3---where programs meet provers
- Mihai Budiu, Joel Galenson and Gordon Plotkin. The Compiler Forest
- Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang and Aditya Nori. A Data Driven Approach for Algebraic Loop Invariants
- Dulma Rodriguez and Martin Hofmann. Automatic Type Inference for Amortised Heap-Space Analysis
- Joost-Pieter Katoen and Doron Peled. Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems
- Jean-Baptiste Jeannin, Dexter Kozen and Alexandra Silva. Language Constructs for Non-Well-Founded Computation
- John Wickerson, Mike Dodds and Matthew Parkinson. Ribbon Proofs for Separation Logic
- Gabriel Scherer and Didier Remy. GADT meet subtyping
- Ivan Lanese, Michael Lienhardt, Claudio Antares Mezzina, Alan Schmitt and Jean-Bernard Stefani. Concurrent Flexible Reversibility