Wednesday, January 26

8:45

Welcome (Tom Ball, Mooly Sagiv)

9:00-10:00

Invited Talk   [Session Chair: Mooly Sagiv]

 Verified squared: does critical software deserve verified tools?

Xavier Leroy, INRIA

10:00-10:30

Break

10:30-12:00

Pointer Analysis   [Session Chair: Ganesan Ramalingam]

Semi-Automated Verification   [Session Chair: David Naumann]

Points-To Analysis with Efficient Strong Updates

O. Lhotak, K. Chung   (Slides)

Relaxed-Memory Concurrency and Verified Compilation

J. Sevcik, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, P. Sewell 

Pick Your Contexts Well: Understanding Object-Sensitivity (The Making of a Precise and Scalable Pointer Analysis)

Y. Smaragdakis, M. Bravenboer, O. Lhotak   (Slides)

Mathematizing C++ Concurrency

M. Batty, S. Owens, S. Sarkar, P. Sewell, T. Weber  (Slides)

Learning Minimal Abstractions

P. Liang, O. Tripp, M. Naik  (Slides)

Formal verification of object layout for C++ multiple inheritance

T. Ramananandro, G. Reis, X. Leroy  (Slides)

12:00-1:30

Lunch

1:30-3:00

Static Analysis   [Session Chair: Ken McMillan]

Semantic Models and Translations   [Session Chair: Philippa Gardner]

Static Analysis for Multi-Staged Programs via Unstaging Translation

W. Choi, B. Aktemur, K. Yi, M. Tatsuta   (Slides)

Step-Indexed Kripke Models over Recursive Worlds

L. Birkedal, B. Reus, J. Schwinghammer, K. Stovring, J. Thamsborg, H. Yang   (Slides)

Static analysis of interrupt-driven programs

M. Schwarz, H. Seidl, V. Vojdani, M. Muller-Olm, P. Lammich  (Slides)

A Kripke Logical Relation Between ML and Assembly

C. Hur, D. Dreyer

A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis

P. Cousot, R. Cousot, F. Logozzo

A typed store-passing translation for general references

F. Pottier   (Slides)

3:00-3:30

Break

3:30-5:00

Shape Analysis   [Session Chair: Radhia Cousot]

Type Abstractions   [Session Chair: Derek Dreyer]

A Shape Analysis for Optimizing Parallel Graph Programs

D. Prountzos, R. Manevich, K. Pingali, K. McKinley   (Slides)

Blame for All

A. Ahmed, R. Findler, J. Siek, P. Wadler  (Slides)

Calling Context Abstraction with Shapes

X. Rival, B. Chang   (Slides)

Correct Blame for Contracts: No More Scapegoating

C. Dimoulas, R. Findler, C. Flanagan, M. Felleisen   (Slides)

Precise Reasoning for Programs Using Containers

I. Dillig, T. Dillig, A. Aiken   (Slides)

Generative type abstraction and type-level computation 

S. Weirich, D. Vytiniotis, S. Peyton-Jones, S. Zdancewic

5:00-7:00

Free Time

7:00-8:00

Appetizers, Drinks, and Xbox/Kinect/Kodu Game Room (Senate)

8:00-9:30

Buffet Dinner and Jazz (Ballroom)

9:30-11:00

Xbox/Kinect/Kodu Game Room (Senate)

Thursday, January 27

9:00-10:00

Invited Talk   [Session Chair: Mooly Sagiv]

The Design of Kodu: A Tiny Visual Programming Language for Children on the Xbox 360

Matthew MacLaurin, Microsoft

10:00-10:30

Break

10:30-12:00

Separation Logic   [Session Chair: Hongseok Yang]

Automata   [Session Chair: Kathleen Fisher]

A separation logic for refining concurrent objects,

A. Turon, M. Wand   (Slides)

The Tree Width of Auxiliary Storage

P. Madhusudan, G. Parlato   (Slides)

Modular Reasoning for Deterministic Parallelism

M. Dodds, S. Jagannathan, M. Parkinson   (Slides)

Fresh-Register Automata

N. Tzevelekos   (Slides)

Expressive Modular Fine-Grained Concurrency Specifications

B. Jacobs, F. Piessens   (Slides)

Vector Addition System Reachability Problem In Less Than 7 Pages

J. Leroux 

12:00-1:30

Lunch

1:30-3:00

Synthesis   [Session Chair: Viktor Kuncak]

Algebra   [Session Chair: Jeff Foster]

Automating String Processing in Spreadsheets using Input-Output Examples

S. Gulwani

Multivariate Amortized Resource Analysis

J. Hoffmann, K. Aehlig, M. Hofmann   (Slides)

Constraint Based Inference of Auxiliary Variables and Relies/Guarantees for Verifying Multi-Threaded Programs

A. Gupta, C. Popeea, A. Rybalchenko   (Slides) 

Elements of Symmetric Lenses

M. Hofmann, B. Pierce, D. Wagner   (Slides)

Geometry of Synthesis III: Resource management through type inference

D. Ghica, A. Smith

Regular Expression Containment: Coinductive Axiomatization and Computational Interpretation

F. Henglein, L. Nielsen   (Slides)

3:00-3:30

Break

3:30-5:00

Model Checking   [Session Chair: Eran Yahav]

Types   [Session Chair: Stephen Freund]

Making Prophecies with Decision Predicates 

B. Cook, E. Koskinen   (Slides)

Dynamic Multirole Session Types

P. Denielou, N. Yoshida   (Slides)

Delay-bounded scheduling

M. Emmi, S. Qadeer, Z. Rakamaric   (Slides)

Practical Affine Types 

J. Tov, R. Pucella  (Slides)

On Interference Abstractions 

N. Sinha, C. Wang   (Slides)

Dynamic Inference of Static Types for Ruby

J. An, A. Chaudhuri, J. Foster, M. Hicks   (Slides)

5:00-5:15

Break

5:15-6:15

Business Session    (Slides for PC Chair's report   and General Chair's report)

6:15-8:00

Break

8:00-10:00

Student Presentation Session (Chair: Byron Cook)

Friday, January 28

9:00-10:00

Invited Session   [Session Chair: Tom Ball]

Robin Milner: Verification, Languages, and Concurrency

Andrew D. Gordon, Peter Sewell

Robert Harper, Alan Jeffrey, John Harrison

10:00-10:30

                                                                                                                                                 Break

10:30-12:00

Complexity   [Session Chair: Madhusudan Parthasarathy]

Medley   [Session Chair: Jan Vitek]

Space Overhead Bounds for Dynamic Memory Management with Partial Compaction

A. Bendersky, E. Petrank

EigenCFA: Accelerating flow analysis with GPUs

T. Prabhu, S. Ramalingam, M. Might, M. Ha   (Slides)

Laws of Order: Expensive Synchronization in Concurrent Algorithms Cannot be Eliminated

H. Attiya, R. Guerraoui, D. Hendler, P. Kuznetsov, M. Michael, M. Vechev

Bisimulation for quantum processes 

Y. Feng, R. Duan, M. Ying   (Slides)

Complexity of Pattern-based Verification for Multithreaded Programs 

J. Esparza, P. Ganty

Safe Nondeterminism in a Deterministic-by-Default Parallel Language 

R. Bocchino, S. Heumann, N. Honarmand, S. Adve, V. Adve, A. Welc, T. Shpeisman

12:00-1:30

Lunch

1:30-3:00

Compilation   [Session Chair: Steve Zdancewic]

Verification   [Session Chair: Sumit Gulwani]

Loop Transformations: Convexity, Pruning and Optimization 

L. Pouchet, U. Bondhugula, C. Bastoul, A. Cohen, J. Ramanujam, P. Sadayappan, N. Vasilache   (Slides)

Verifying Higher-Order Programs with Pattern-Matching Algebraic Data Types 

C. Ong, S. Ramsay  (Slides)

The Essence of Compiling with Traces

S. Guo, J. Palsberg

Streaming Transducers for Algorithmic Verification of Single-Pass List Processing Programs

R. Alur, P. Cerny

Resourceable, Retargetable, Modular Instruction Selection Using a Machine-Independent, Type-Based Tiling of Low-Level Intermediate Code 

N. Ramsey, J. Dias  (Slides)

Decidable logics combining heap structures and data

P. Madhusudan, G. Parlato, X. Qiu   (Slides)

3:00-3:30

Break

3:30-4:00

[Session Chair: Michael Hicks]

A Technique for the Effective and Automatic Reuse of Classical Compiler Optimizations on Multithreaded Code

P. G. Joisha, R. S. Schreiber, P. Banerjee, Hans-J. Boehm, D. R. Chakrabarti   (Slides)

4:00-4:15

Wrap-up and Xbox/Kinect Raffle Drawing