ESOP 2013

32 papers

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