Preliminary Session Schedule

Day/TimeTitlePapers
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
16:00-17:30
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
10:30-12:30
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
14:00-15:00
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
16:30-18:00
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
10:30-12:30
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
15:15-16:15
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
16:30-18:00
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
11:00-12:30
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
14:00-15:00
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
16:30-18:00
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