ETAPS 2013: 16-24 March 2013, Rome, Italy

ESOP 2013 accepted papers

You can find information about LNCS proceedings (LNCS 7792) at http://www.springeronline.com/978-3-642-37035-9 or access the online version at http://www.springerlink.com/content/978-3-642-37035-9/.

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