Program of Monday, April 2nd

 9.00
 9.30
Welcome
 9.30
10.30

Session chair: Furio Honsell
Gordon Plotkin (Invited Lecture)
10.30
11.00
Coffee
11.00
12.30
CC
Program Analysis 1
Session chair: Tom Reps

Alias Analysis by means of a Model Checker
Vincenzo Martena, Pierluigi Sanpietro (Politecnico di Milano)

Points-to and Side-effect Analyses for Programs Built with Precompiled Libraries
Atanas Rountev, Barbara G. Ryder (Rutgers University)

A Novel Probabilistic Data-Flow Framework
Eduard Mehofer (University of Vienna),
Bernhard Scholz (Vienna University of Technology)

FOSSACS
Concurrency and Mobility
Session chair:
Luca Cardelli

Secrecy Types for Asymmetric Communication
Martin Abadi (Bell Labs Research),
Bruno Blanchet (INRIA Rocquencourt)

High-Level Petri Nets as Type Theories in the Join Calculus
Maria Grazia Buscemi, Vladimiro Sassone (Università di Catania)

The Complexity of Model Checking Mobile Ambients
Witold Charatonik (Max-Planck-Institut für Informatik and University of Wroclaw)
Silvano Dal Zilio, Andrew D. Gordon (Microsoft Research),
Supratik Mukhopadhyay, Jean-Marc Talbot (Max-Planck-Institut für Informatik)

TACAS
Opening: Tiziana Margaria and Wang Yi

Symbolic Verification
Session chair: Tiziana Margaria

Language Containment Checking with Nondeterministic BDDs
Bernd Finkbeiner (Stanford University)

Satisfiability Checking Using Boolean Expression Diagrams
Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard (IT University of Copenhagen)

A Library for Composite Symbolic Representations
Tuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan (University of California)

WADT
12.30
15.00
Lunch
15.00
17.00
CC
Program Transformation
Session chair: Uwe Assmann

Imperative Program Transformation by Rewriting
David Lacey, Oege de Moor (Oxford University)

Compiler Transformation of Pointers to Explicit Array Accesses in DSP Applications
Bjoern Franke, Michael O'Boyle (University of Edinburgh)

User-extensible Simplification — Type-based Optimizer Generators
Sibylle Schupp, Douglas Gregor, David Musser (Rensselaer Polytechnic Institute),
Shin-Ming Liu (Hewlett Packard)

A Practical, Robust Method for Generating Variable Range Tables
Caroline Tice (Compaq Systems Research Center),
Susan L. Graham (University of California, Berkeley)

FOSSACS
Type Theory
Session chair:
Pawel Urzyczy

Type inference with recursive type equations
Mario Coppo (Università di Torino)

Axioms for Recursion in Call-by-Value
Masahito Hasegawa, Yoshihiko Kakutani (Kyoto University)

Type Isomorphisms and Proof Reuse in Dependent Type Theory
Gilles Barthe (INRIA), Olivier Pons (Universidade do Minho)

The Rho Cube
Horatiu Cirstea (LORIA and UHP),
Claude Kirchner (LORIA and INRIA),
Luigi Liquori (LORIA and INPL)

TACAS
Infinite State Systems: Deduction and Abstraction
Session chair: Rance Cleaveland

Synthesis of Linear Ranking Functions
Michael A. Colón, Henny B. Sipma (Stanford University)

Automatic Deductive Verification with Invisible Invariants
Amir Pnueli, Sitvanit Ruah (Weizmann Institute),
Lenore Zuck (New York University)

Incremental Verification by Abstraction
Yassine Lakhnech, S. Bensalem (VERIMAG),
S. Berezin (Carnegie Mellon University),
S. Owre (SRI International)

A Technique for Invariant Generation
A. Tiwari, H. Ruess, H. Saidi, N. Shankar (SRI International)

WADT
17.00
17.30
Coffee
17.30
19.00
CC
Program Analysis 2
Session chair: Reinhard Wilhelm

Efficient Symbolic Analysis for Optimizing Compilers
Robert A. van Engelen (Florida State University)

Interprocedural Shape Analysis for Recursive Programs
Noam Rinetzky (Technion Haifa),
Mooly Sagiv (Tel-Aviv University)

Design-Driven Compilation
Radu Rugina, Martin Rinard (Massachusetts Institute of Technology)

FOSSACS
Formal Verification
Session chair:
Carolyn Talcott

Verified Bytecode Verifiers
Tobias Nipkow (Technische Universität München)

Higher-Order Abstract Syntax with Induction in Isabelle/HOL:
Formalizing the Pi-Calculus and Mechanizing the Theory of Contexts

Christine Röckl (Technische Universität München),
Daniel Hirschkoff (LIP, ENS de Lyon),
Stefan Berghofer (Technische Universität München)

Marrella and the Verification of an Embedded System (DEMO)
Dominique Ambroise, Patrick Auge (Université de Paris Sud),
Kamel Bouchefra (Université Paris 13),
Brigitte Rozoy (Université de Paris Sud)

TACAS
Applications of Model Checking Techniques
Session chair: John Hatcliff

Model Checking Syllabi and Student Careers
Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia (Università di Trento)

Verification of Vortex Workflows
Xiang Fu, Tevfik Bultan, Jianwen Su (University of California)

Parameterized Verification of Multithreaded Software Libraries
Thomas Ball, Sagar Chaki, Sriram K. Rajamani (Microsoft Research)

WADT
20.00 Reception