SUNDAY, August 9, 2009

Invited talk 09:00-10:00 (Chair: Jens Palsberg)

Ras Bodik, University of California, Berkeley

"Algorithmic Program Synthesis with Partial Programs and Decision Procedures"

Session 1   10:30-12:30 (Chair: Anders Møller)

Abstraction Refinement for Quantified Array Assertions
    Mohamed Nassim Seghir
    Andreas Podelski
    Thomas Wies

Infer Dataflow Properties of User Defined Table Processors
    Songtao Xia
    Manuel Fahndrich
    Francesco Logozzo

Polymorphic Fractional Capabilities
    Hirotoshi Yasuoka
    Tachio Terauchi

Automatic Parallelization and Optimization of Programs by Proof Rewriting
    Clément Hurlin

Session 2   14:00-15:30 (Chair: David Schmidt)

Refinement of Trace Abstraction
    Matthias Heizmann
    Jochen Hoenicke
    Andreas Podelski

The Causal Graph Revisited For Directed Model Checking
    Martin Wehrle
    Malte Helmert

Proving the correctness of the implementation of a control command algorithm
    Olivier Bouissou

Hammer Museum   16:00-17:00

SAS Dinner   18:00-21:00

The visit to the Hammer Museum includes a choice of two guided tours.

The SAS Dinner will be held at Napa Valley Grille, 1100 Glendon Avenue, Los Angeles, CA 90024; phone: 310-824-3322. Napa Valley Grille is across the street from the Hammer Museum. We can socialize in the dinner room from 17:00.

If you drive to Hammer Museum and/or the SAS dinner, you can use the valet parking at Napa Valley Grille; show your valet ticket in the restaurant and they will make sure you don't have to pay.

MONDAY, August 10, 2009

Invited talk 09:00-10:00 (Chair: Zhendong Su)

Shaz Qadeer, Microsoft Research

"Algorithmic Verification of Systems Software Using SMT Solvers"

Session 3   10:30-12:30 (Chair: Eran Yahav)

Abstract Interpretation of FIFO Caches
    Daniel Grund
    Jan Reineke

A Verifiable, Control Flow Aware Constraint Analyzer for Bounds Check Elimination
    David Niedzielski
    Jeffery von Ronne
    Andreas Gampe
    Kleanthis Psarris

Increasing the scope and resolution of Interprocedural Static Single Assignment
    Silvian Calman
    Jianwen Zhu

Region Analysis for Race Detection
    Helmut Seidl
    Vesal Vojdani

Session 4   14:00-15:30 (Chair: Joxan Jaffar)

Bottom-up Shape Analysis
    Bhargav Gulavani
    Supratik Chakraborty
    Ganesan Ramalingam
    Aditya Nori

The Complexity of Andersen's Analysis in Practice
    Manu Sridharan
    Stephen J. Fink

Optimizing Pointer Analysis Using Bisimilarity
    Luke Simon

Session 5   16:00-17:30 (Chair: Naoki Kobayashi)

Type Analysis for JavaScript
    Simon Holm Jensen
    Anders Møller
    Peter Thiemann

Abstract parsing: static analysis of dynamically generated string output using LR-parsing technology
    Kyung-Goo Doh
    Hyunha Kim
    David Schmidt

Creating transformations for matrix obfuscation
    Stephen Drape
    Irina Voiculescu

TUESDAY, August 11, 2009 (Joint LICS/SAS)

LICS/SAS Joint invited talk 08:30-09:30 (Chair: Andrew Pitts)

Edmund M. Clarke, Carnegie Mellon University

"Model Checking: My 27 Year Quest to Conquer the State-Explosion Problem"

Session 1   09:30-10:30 (Chair: Andrew Pitts)

The General Vector Addition System Reachability Problem by Presburger Inductive Invariants (LICS)
    Jerome Leroux

Abstract Interpretation from a Topological Perspective (SAS)
    David Schmidt

Session 2   11:00-12:30 (Chair: Radhia Cousot)

Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships (SAS)
    Liqian Chen
    Antoine Mine
    Ji Wang
    Patrick Cousot

Invariant Checking for Programs with Procedure Calls (SAS)
    Guillem Godoy
    Ashish Tiwari

Proving Inter-Program Properties (SAS)
    Andrei Voronkov
    Iman Narasamdya

Session 3   14:00-15:30 (Chair: Martin Abadi)

(14:00-15:00) Invited Tutorial: Applications of Game Semantics: From Program Analysis to Hardware Synthesis (LICS)
    Dan Ghica

(15:00-15:30) Boundedness vs. Unboundedness of Lock Chains: Characterizing Decidability of CFL-Reachability for Threads Communicating via Locks (LICS)
    Vineet Kahlon

Session 4   16:00-17:30 (Chair: Gopalan Nadathur)

Psi-calculi: Mobile processes, Nominal Data and Logic (LICS)
    Joachim Parrow
    Magnus Johansson
    Björn Victor
    Jesper Bengtson

An Algebra for Kripke Polynomial Coalgebras (LICS)
    Marcello Bonsangue
    Jan Rutten
    Alexandra Silva

Trace Semantics Is Fully Abstract (LICS)
    Sumit Nain
    Moshe Vardi

LICS Short Talks   17:30-18:00 (Chair: Andre Scedrov)

Efficient Parallel Path Checking
    Lars Kuhtz

Reachability and Safety Games on Vector Addition Systems with States
    Tomas Brazdil
    Petr Jancar
    Antonin Kucera

A Time and Space Efficient Simulation Algorithm
    Francesco Ranzato
    Francesco Tapparo