Preliminary Session Schedule

Session 0: Tue 19 Mar 2013
14:00-14:03; 14:03-15:30
Philippa Gardner; Matthias Felleisen
Programming Techniques

Mihai Budiu, Joel Galenson, Gordon D. Plotkin
The Compiler Forest
Microsoft Research Silicon Valley; University of California at Berkeley; University of Edinburgh

Arthur Charguéraud
Pretty-Big-Step Semantics
INRIA Saclay; Université Paris Sud; CNRS

Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva
Language Constructs for Non-Well-Founded Computation
Cornell University; Radboud University Nijmegen

Session 1: Tue 19 Mar 2013
Matthias Felleisen
Programming Tools

Stephen Chang
Laziness by Need
Northeastern University

Kazutaka Matsuda, Meng Wang
FliPpr: A Prettier Invertible Printing System
The University of Tokyo; Chalmers University of Technology

María Alpuente, Demis Ballis, Francisco Frechina, Julia Sapiña
Slicing-based Trace Analysis of Rewriting Logic Specifications with iJulienne
Universitat Politècnica de València; Università degli Studi di Udine

Jean-Christophe Filliâtre, Andrei Paskevich
Why3---Where Programs Meet Provers
Université Paris Sud; CNRS; INRIA Saclay

Session 2: Wed 20 Mar 2013
Philippa Gardener
Separation Logic

Constantin Enea, Vlad Saveluc, Mihaela Sighireanu
Compositional Invariant Checking for Overlaid and Nested Linked Lists
Université Paris Diderot; Sorbonne Paris Cite

Ioannis T. Kassios, Eleftherios Kritikos
A Discipline for Program Verification based on Backpointers and its Use in Observational Disjointness
ETH Zurich; National Technical University of Athens

Kasper Svendsen, Lars Birkedal, Matthew Parkinson
Modular Reasoning about Separation of Concurrent Data Structures
IT University of Copenhagen; Microsoft Research Cambridge

John Wickerson, Mike Dodds, Matthew Parkinson
Ribbon Proofs for Separation Logic
Technische Universität Berlin; University of York; Microsoft Research Cambridge

Session 3: Wed 20 Mar 2013
Holger Hermanns
Gradual Typing

Niki Vazou, Patrick M. Rondon, Ranjit Jhala
Abstract Refinement Types
UC San Diego; Google

Asumu Takikawa, T. Stephen Strickland, Sam Tobin-Hochstadt
Constraining Delimited Control with Contracts
Northeastern University; University of Maryland at College Park

Session 4: Wed 20 Mar 2013
Martin Hofmann
Shared-memory Concurrency and Verification

Alexey Gotsman, Noam Rinetzky, Hongseok Yang
Verifying Concurrent Memory Reclamation Algorithms with Grace
IMDEA Software Institute; Tel-Aviv University; University of Oxford

Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer
Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
Imperial College London; Microsoft Research Cambridge

Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
Verifying Concurrent Programs against Sequential Specifications
Université Paris Diderot

Session 5: Thu 21 Mar 2013
Yannis Smaragdakis
Process Calculi

Kirstin Peters, Uwe Nestmann, Ursula Goltz
On Distributability in Process Calculi
TU Berlin; TU Braunschweig

Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho
Behavioral Polymorphism and Parametricity in Session-Based Communication
Universidade Nova de Lisboa; Carnegie Mellon University

Bernardo Toninho, Luís Caires, Frank Pfenning
Higher-Order Processes, Functions, and Sessions: A Monadic Integration
Carnegie Mellon University; Universidade Nova de Lisboa

Ivan Lanese, Michael Lienhardt, Claudio Antares Mezzina, Alan Schmitt, Jean-Bernard Stefani
Concurrent Flexible Reversibility
University of Bologna; Paris Diderot University; FBK, Trento; INRIA

Session 6: Thu 21 Mar 2013
Didier Remy
Taming Concurrency

Yi Lu, John Potter, Jingling Xue
Structural Lock Correlation with Ownership Types
University of New South Wales at Sydney

Joost-Peter Katoen, Doron Peled
Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems
RWTH Aachen University; University of Twente; Bar Ilan University Ramat Gan

Session 7: Thu 21 Mar 2013
Ranjit Jhala
Model Checking and Verification

Naoki Kobayashi, Atsushi Igarashi
Model-Checking Higher-Order Programs with Recursive Types
The University of Tokyo; Kyoto Univeristy

Mohamed Nassim Seghir, Daniel Kroening
Counterexample-guided Precondition Inference
University of Oxford

Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith
Information Reuse for Multi-goal Reachability Analyses
University of Passau; Vienna University of Technology; University of Oxford; Queen Mary University of London

Session 8: Fri 22 Mar 2013
Scott Owens
Weak-memory Concurrency and Verification

Radha Jagadeesan, Gustavo Petri, Corin Pitcher, James Riely
Quarantining Weakness
DePaul University; Purdue University

Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig
Software Verification for Weak Memory via Program Transformation
University College London; University of Oxford; Queen Mary University of London

Ahmed Bouajjani, Egor Derevenetc, Roland Meyer
Checking and Enforcing Robustness against TSO
University Paris 7; Fraunhofer ITWM; University of Kaiserslautern

Session 9: Fri 22 Mar 2013
Philippa Gardner
Special ETAPS Session: Invited Talk

Mark S. Miller, Tom Van Cutsem, Bill Tulloh
Distributed Electronic Rights in JavaScript
Google; Vrije Universiteit Brussel

Session 10: Fri 22 Mar 2013
Annie Liu
Types, Inference, and Analysis

Gabriel Scherer, Didier Rémy
GADTs meet subtyping
INRIA Rocquencourt

Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, Aditya V. Nori
A Data Driven Approach for Algebraic Loop Invariants
Stanford University; University of California at Berkeley; Microsoft Research India

Martin Hofmann, Dulma Rodriguez
Automatic Type Inference for Amortised Heap-Space Analysis
University of Munich; Monoidics Ltd