09.00 - 9.30: 	Welcome, etc
  09.30 - 10.30: 	FIRST MORNING SESSION
  ESOP	Invited Lecture:
  	Resources, Concurrency and Local Reasoning
  	Peter O'Hearn, Queen Mary, University of London
  10.30 - 11.00: 	coffee
  11.00 - 12.30: 	SECOND MORNING SESSION
  	Revisiting Positive Equality
  	Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur
  	An Interpolating Theorem Prover
  	Kenneth McMillan 
  	Minimal Satisfying Assignments for Bounded Model Checking
  	Fabio Somenzi, Kavita Ravi
  FASE: Objects and Aspects
  	Consistent Adaptation and Evolution of Class Diagrams during Refinement	
  	Alexander Egyed	(Teknowledge Corporation)
  	Measuring Aspect Cohesion	
  	Jianjun Zhao (Fukuoka Institute of Technology), Baowen Xu (Southeast University)
  	Refactoring Object-Z Specifications	
  	Tim McComb (The University of Queensland)
  ESOP: Abstract Interpretation
  	Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors
  	Antoine Min\'e, Ecole Normale Sup\'erieure de Paris
  	Strong preservation as completeness in abstract interpretation
  	Francesco Ranzato and Francesco Tapparo, Universit\`a di Padova
  	Static Analysis of Digital Filters
  	J\'er\^ome Feret , Ecole Normale Sup\'erieure de Paris
  12.30 - 14.30:	LUNCH
  	Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study
  	Håkan Younes, Marta Kwiatkowska, Gethin Norman, David Parker
  	Efficient computation of time-bounded reachability probabilities in
  	uniformized continuous-time Markov decision processes
  	Holger Hermanns, Christel Baier , Boudewijn R. Haverkort , Joost-Pieter Katoen
  	Model Checking Discounted Temporal Properties
  	Luca de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga
  FASE: Smart Cards
  	Checking Absence of Illicit Applet Interactions: A Case Study	
  	Marieke Huisman (INRIA Sophia-Antipolis), Dilian Gurov (Royal
  	Institute of Technology Kista), Christoph Sprenger (INRIA Sophia-Antipolis), 
  	Gennady Chugunov (Swedish Institute of Computer Science Kista) 
  	A Tool-Assisted Framework for Certified Bytecode Verification
  	Gilles Barthe, Guillaume Dufay (INRIA Sophia-Antipolis)
  	Reasoning about Card Tears and Transactions in Java Card	
  	Engelbert Hubbers, Erik Poll (University of Nijmegen)
  ESOP: Modular and staged languages:
  	Sound and Decidable Type Inference for Functional Dependencies
  	Gregory J. Duck, University of Melbourne,Simon Peyton-Jones, Microsoft Research,
  	Peter J. Stuckey, University of Melbourne, and Martin Sulzmann, National 
  	University of Singapore
  	Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types
  	Tom Hirschowitz, Ecole Normale Sup\'erieure de Lyon, Xavier Leroy, 
  	INRIA Rocquencourt, and J. B. Wells, Heriot-Watt University
  	ML-like Inference for Classifiers
  	Cristiano Calcagno, Imperial College London, Eugenio Moggi, 
  	Universit\'a di Genova, Walid Taha, Rice University
  16.30 - 17.00: 	coffee
  	Automatic Creation of Environment Models via Training
  	Thomas Ball, Vladimir Levin, Fei Xie
  	Error Explanation with Distance Metrics
  	Alex Groce
  	Online Efficient Predictive Safety Analysis of Multithreaded Programs
  	Rosu, Grigore
  	Koushik Sen, Gul Agha
  FASE: Components I
  	Predictable Dynamic Plugin Systems	
  	Robert Chatley,	Susan Eisenbach, Jeff Kramer, Jeff Magee, Sebastian
  	Uchitel (Imperial College London)
  	A Correlation Framework for the CORBA Component Model	
  	Georg Jung, John Hatcliff, Venkatesh Prasad Ranganath (Kansas State
  	Cadena: An Integrated Development Environment for Analysis, Synthesis,
  	and Verification of Component-based Systems
  	Adam Childs, Jesse Greenwald, Venkatesh Ranganath,
  	Xianghua Deng, Matthew Dwyer, John Hatcliff, Georg Jung, Prashant
  	Shanti, Gurdip Singh (Kansas State University)
  ESOP: Constraint, logic, and pattern programming
  	From Constraints to Finite Automata to Filtering Algorithms
  	Mats Carlsson and Nicolas Beldiceanu,
  	Swedish Institute of Computer Science, Uppsala
  	A Memoizing Semantics for Functional Logic Languages
  	Espa{\~n}a-Boquera, Salvador  Vicent Estruch
  	Technical University of Valencia
  	Adaptive Pattern Matching on Binary Data
  	Per Gustafsson and Konstantinos Sagonas, Uppsala University
  09.00 - 10.00: 	FIRST MORNING SESSION IS (Gruia)
  FASE	Invited Lecture:
  	A Formal Treatment of Context-Awareness
  	Gruia-Catalin Roman, Washington University
  10.00 - 10.30: 	coffee
  10.30 - 12.30:  SECOND MORNING SESSION
  TACAS: Tools
  	Vooduu: Verification of Object-Oriented Designs Using UPPAAL
  	Karsten Diethers, Michaela Huhn 
  	CoPS - Checker of Persistent Security
  	Sabina Rossi, Carla Piazza, Enrico Pivato
  	Tampere Verification Tool
  	Henri Hansen, Heikki Virtanen, Henri Hansen, Antti Valmari, 
  	Juha Nieminen, Timo Erkkilä
  	SyncGen: An Aspect-Oriented Framework for Automatically Generating 
  	Synchronization Implementations from High-Level Specifications
  	John Hatcliff, Xianghua Deng, Matthew Dwyer, Masaaki Mizuno
  	MetaGame: An Animation Tool for Model-Checking Games
  	Markus Müller-Olm, Haiseung Yoo
  	A Tool for Checking ANSI-C Programs
  	Daniel Kroening, Edmund Clarke, Flavio Lerda 
  FASE: Security and Web Services
  	Actor-Centric Modeling of User Rights	
  	Ruth Breu (Universität Innsbruck), Gerhard Popp (Technische
  	Universität München)
  	Modeling Role-Based Access Control Using Parameterized UML Models	
  	Dae-Kyoo Kim, Indrakshi Ray, Robert France, Na Li (Colorado State
  	Compositional Nested Long Running Transactions	
  	Laura Bocchi (University of Bologna)
  	DaGen: A Tool for Automatic Translation from DAML-S to High-level Petri Nets
  	Daniel Moldt, Jan Ortmann (University of Hamburg)
  ESOP: Spatial logics
  	Compositional Analysis of Authentication Protocols 
  	Michele Bugliesi, Riccardo Focardi, and  Matteo Maffei,
  	Univserit\`a C\'a Foscari di Venezia
  	A Distributed Abstract Machine for Boxed Ambient Calculi
  	Andrew Phillips, Nobuko Yoshida, and Susan Eisenbach,
  	Imperial College, London
  	A Dependently Typed Ambient Calculus
  	Cedric Lhoussaine and Vladimiro Sassone, University of Sussex
  	A Control Flow Analysis for Safe and Boxed Ambients
  	Francesca Levi, Universit\'a di Genova, and Chiara Bodei, Universit\`a di Pisa
  12.30 - 14.30: 	LUNCH
  14.30 - 16.30:  FIRST AFTERNOON SESSION	
  FASE: Modeling and Requirements
  	Integrating Meta Modelling Aspects with Graph Transformation for
  	Efficient Visual Language Definition and Model Manipulation
  	Roswitha Bardohl, Hartmut Ehrig (Technische Universität Berlin), 
  	Juan de Lara (Universidad Autónoma de Madrid), Gabriele
  	Taentzer (Technische Universität Berlin)
  	An Operational Semantics for Stateflow	
  	Grégoire Hamon,	John Rushby (SRI International)
  	Improving Use Case Based Requirements Using Formally Grounded Specifications
  	Christine Choppy (Université Paris XIII), Gianna Reggio (Università di
  	The GOPCSD Tool: An Integrated Development Environment for Process
  	Control Requirements and Design	
  	Islam A.M. El-Maddah, Tom S.E. Maibaum (King's College London)
  ESOP: Distributed programming
  	Linear Types for Packet Processing
  	Robert Ennals, Intel Research,Richard Sharp and Alan Mycroft, 
  	Cambridge University
  	Modal Proofs As Distributed Programs
  	Limin Jia and David Walker, Princeton University
  	ULM, A Core Programming Model for Global Computing
  	Gerard Boudol, INRIA, Sophia Antipolis
  	A Semantic Framework for Designer Transactions
  	Jan Vitek, Suresh Jagannathan, Adam Welc, Antony L. Hosking,
  	Purdue University
  FOSSACS: Specification Formalisms
  	Partial Correctness Assertions Provable in Dynamic Logics
  	D. Leivant
  	Choice in Dynamic Linking
  	M. Abadi, G. Gonthier and B. Werner
  	Specifying and Verifying Partial Order Properties using Template MSCs
  	B. Genest, M. Minea, A. Muscholl and D. Peled
  	Reasoning about Dynamic Policies
  	R. Pucella and V. Weissman
  16.30 - 17.00:  coffee
  	Obtaining Memory-Efficient Reachability Graph Representations Using the
  	Sweep-Line Method
  	Michael Westergaard, Thomas Mailund
  	Automated generation of a progress measure for the sweep-line method
  	Karsten Schmidt 
  	Tarjan's Algorithm Makes On-the-fly LTL Verification More Efficient
  	Jaco Geldenhuys, Antti Valmari
  FASE: Testing
  	Automated Debugging using Path-Based Weakest Preconditions
  	Haifeng He, Neelam Gupta (The University of Arizona)
  	Filtering TOBIAS combinatorial test suites	
  	Yves Ledru, Lydie du Bousquet, Olivier Maury, Pierre Bontron (IMAG)
  	Systematic Testing of Software Architectures in the C2 style	
  	Henry Muccini (Università degli Studi dell'Aquila), Marcio
  	Dias (University of California at Irvine), D.J. Richardson
        (University of California)
  ESOP: Logics and typing
  	Semantical Analysis of Specification Logic, An Operational Approach
  	Dan Ghica, Oxford University
  	Answer Type Polymorphism in Call-by-name Continuation Passing
  	Hayo Thielecke, University of Birmingham
  	System E: Expansion Variables for Flexible Typing with Linear
  	and Non-linear Types and Intersection Types
  	Sebastian Carlier, Jeff Polakow, J. B. Wells, Heriot-Watt University,
  	and A. J. Kfoury, Boston University
  09.00 - 10.00: 	FIRST MORNING SESSION IS 
  ETAPS	Invited Lecture:
  10.00 - 10.30: 	coffee
  10.30 - 12.30:	SECOND MORNING SESSION 
  FASE: Model Checking and Analysis
  	Optimising Communication Structure for Model Checking	
  	Peter Saffrey (University College London), Muffy Calder (University of
  	Translating Software Designs for Model Checking	
  	Fei Xie (University of Texas at Austin), Vladimir Levin (Microsoft),
  	Robert P. Kurshan (Cadence), James C. Browne (University of Texas at
  	Enhancing Remote Method Invocation through Type-Based Static Analysis	
  	Carlo Ghezzi, Vincenzo Martena, Gian Pietro Picco (Politecnico di
  	Specification and Analysis of Real-Time Systems Using Real-Time Maude	
  	Peter Csaba Ölveczky (University of Illinois at Urbana-Champaign and
  	University of Oslo), José Meseguer (University of Illinois at
  ESOP: Security
  	A Hardest Attacker for Leaking References
  	Rene Rydhof Hansen, Technical University of Denmark
  	Trust Management in Strand Spaces: A Rely-Guarantee Method
  	Joshua Guttman, Javier Thayer, Jay Carlson, Jonathan Herzog,
  	John Ramsdell, Brian Sniffen, MITRE Corporation
  	Just Fast Keying in the Pi Calculus
  	Martin Abadi, University California Santa Cruz,
  	Bruno Blanchet, Ecole Normale Sup\'erieure de Paris and
  	Max-Institut f\"ur Informatik Saarbr\"ucken,
  	and C\'edric Fournet, Microsoft Research
  	Decidable Analysis of Cryptographic Protocols with Products and
  	Modular Exponentiation
  	Vitaly Shmatikov, SRI International
  FOSSACS: Process Algebra and Distributed Computing
  	Election and Local Computations on Edges (Extended Abstract)
  	J. Chalopin and Y. Métivier
  	Finite Alphabets versus Omega-Completeness: From Ready Pairs to Ready Traces
  	W. Fokkink and S. Nain
  	Bisimulation on Speed: Lower Time Bounds
  	G. Lüttgen and W. Vogler
  	On the Expressiveness of CCS-like Calculi
  	P. Giambiagi, G. Schneider, and F.D. Valencia
  12.30 - 14.30: 	LUNCH
  14.30 - 15.30: 	FIRST AFTERNOON SESSION IS (Comon)
  FOSSACS Invited Lecture:
  	Resource-Optimal Scheduling Using Priced Timed Automata
  	Jacob Rasmussen, Kim G. Larsen, K. Subramani
  	Decidable and Undecidable Problems in Schedulability Analysis Using Timed
  	Yi Wang, Pavel Krcal
  FASE: Components II
  	A Systematic Methodology for Developing Component Frameworks	
  	Si Won Choi, Soo Ho Chang, Soo Dong Kim (Soongsil University)
  	Automating Decisions in Component Composition Based on Propagation of
  	Ioana Sora, Vladimir Cretu (University Politehnica of Timisoara),
  	Pierre Verbaeten, Yolande Berbers (Katholieke Universiteit Leuven)
  FOSSACS: Probabilistic Aspects
  	Perfect-information Stochastic Parity Games
  	W. Zielonka
  	Duality for Labelled Markov Processes
  	M. Mislove, J. Ouaknine, D. Pavlovic and J. Worrell
  16.30 - 17.00: coffee
  	The Succinct Solver Suite
  	Henrik Pilegaard, Flemming Nielson, Hanne Riis Nielson, Sun Hongyan, Mikael
  	René Buchholtz, Rydhof Hansen, Helmut Seidl
  	Binding-Time Analysis for MetaML via Type Inference and Constraint Solving
  	Nathan Linger, Tim Sheard
  	A Class of Polynomially Solvable Range Constraints for Interval Analysis
  	without Widenings and Narrowings
  	Zhendong Su, David Wagner
  ESOP: Validation
  	Functors for Proofs and Programs
  	Jean-Christophe Filliatre and Pierre Letouzey, LRI-CNRS Universit\'e Paris-Sud
  	Extracting a Data Flow Analyser in Constructive Logic
  	David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu
  	IRISA and ENS Cachan
  	Canonical Graph Shapes
  	Arend Rensink, University of Twente
  FOSSACS: Security 
  	On the Existence of an Effective and Complete Inference System for
  	Cryptographic Protocols 
  	L. Bozga, C. Ene and Y. Lakhnech,
  	A Note on the Perfect Encryption Assumption in a Process Calculus
  	P. Degano and R. Zunino,
  	Probabilistic Bisimulation and Equivalence for Security Analysis of
  	Network Protocols 
  	A. Ramanathan, J. Mitchell, A. Scedrov and V. Teague
  09.00 - 10.00: FIRST MORNING SESSION IS (Valmari)
  TACAS	Invited Lecture:
  	What the Small Rubik's Cube Taught Me on Data Structures,
  	Information Theory and Randomisation
  	Antti Valmari, Tampere University of Technology (Finland)
  10.00 - 10.30: coffee
  10.30 - 12.30: SECOND MORNING SESSION 
  CC: Program Analysis
  	Analyzing memory accesses in x86 executables, 
  	Gogul Balakrishnan and Thomas Reps, University of Wisconsin, Madison, USA.
  	The limits of alias analysis for scalar optimizations, 
  	Rezaul A. Chowdhury, Peter Djeu, University of Texas, Austin, USA, 
  	Brendon Cahoon, Conformative Systems, Austin, USA, James H. Burrill, 
  	University of Massachusetts, Amherst, USA, and Kathryn S. McKinley,University of Texas, Austin, USA.
  	Pruning interference and ready dependence for slicing concurrent Java programs, 
  	Venkatesh Prasad Ranganath and John Hatcliff, Kansas State University, USA.
  	Data dependence profiling for speculative optimizations, 
  	Tong Chen, Jin Lin, Xiaorun Dai, Wei-Chung Hsu, and Pen-Chung Yew, University of Minnesota, USA.
  	A Partial Order Semantics Approach to the Clock Explosion Problem of
  	Timed	Automata
  	Peter Niebert, Sarah Zennou, Denis Lugiez
  	Lower and Upper Bounds in Zone Based Abstractions of Timed Automata
  	Gerd Behrmann, Patricia Bouyer, Kim G. Larsen, Radek Pelánek
  	A Scalable Incomplete Test for the Boundedness of UML RT Models
  	Stefan Leue, Richard Mayr, Wei Wei
  	Automatic Verification of Time-Sensitive Cryptographic Protocols
  	Giorgio Delzanno, Pierre Ganty
  FOSSACS: Categorical Generalizations
  	Deriving Bisimulation Congruences in the DPO Approach to Graph Rewriting
  	H. Ehrig and B. Koenig
  	Adhesive Categories
  	S. Lack and P. Sobocinski
  	Canonical Models for Computational Effects
  	J. Power
  	Unifying Recursive and Co-recursive Definitions in Sheaf Categories
  	P. Di Gianantonio and M. Miculan
  12.30 - 14.30: LUNCH
  CC	Invited Lecture:
  CC: Parsing
  	Elkhound: a fast, practical GLR parser generator, 
  	Scott McPeak and George Necula, Berkeley, USA.
  	Generalised parsing: some engineering costs, 
  	Adrian Johnstone, Elizabeth Scott, and Giorgios Economopoulos, University of London, UK.
  	Simulation-Based Verification of Autonomous Controllers with
  	Livingstone PathFinder
  	Tony Lindsey, Charles Pecheur
  	Automatic Parametric Verification of Root Contention Protocol based on
  	Abstract State Machines and First Order Timed Logic
  	Daniele Beauquier, Tristan Crolard, Evguenia Prokofieva
  FOSSACS: Rewriting
  	Polynomials for Proving Termination of Context-Sensitive Rewriting
  	S. Lucas
  	On Term Rewriting Systems Having a Rational Derivation
  	A. Meyer
  16.30 - 17.00:  coffee
  17.00 - 18.30:  THIRD AFTERNOON SESSION 
  CC: Loop Analysis
  	An automata-theoretic algorithm for counting solutions to Presburger formulas, 
  	Erin Parker, University of North Carolina, Chapel Hill, USA and 
  	Siddhartha Chatterjee, IBM T.J.Watson Research Center, USA.
  	A symbolic approach to Bernstein expansion for program analysis and optimization, 
  	Irina Tchoupaeva, Universite Strasbourg, France, and 
  	Philippe Clauss, INRIA Rocquencourt, France.
  	Periodic polyhedra, 
  	Benoît Meister, LSIIT-ICPS, Illkirch, France.
  	Refining approximations in software predicate abstraction
  	Byron  Cook, Thomas Ball, Satyaki Das, Sriram K. Rajamani
  	Checking Strong Specifications Using An Extensible Software Model-checking
  	Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff
  	Applying Game Semantics to Compositional Software Modeling and
  	Dan Ghica, Samson Abramsky, Andrzej Murawski, Luke Ong
  FOSSACS: Automata Theory and Logic
  	Distance Desert Automata and the Star Height One Problem (Extended Abstract)
  	D. Kirsten
  	Tree Transducers and Tree Compressions
  	S. Maneth and G. Busatto
  	On Recognizable Timed Languages
  	O. Maler and A. Pnueli
  	LTL over Integer Periodicity Constraints (extended abstract)
  	S. Demri
  09.00 - 10.00: 	FIRST MORNING SESSION IS (Milner)
  ETAPS	Invited Lecture:
  10.00 - 10.30: 	coffee
  10.30 - 12.30: 	SECOND MORNING SESSION
  CC: Optimization
  	Region-based partial dead code elimination on predicated code, 
  	Qiong Cai, Lin Gao, Jingling Xue, University of New South Wales, Sydney, Australia.
  	Value-based partial redundancy elimination, 
  	Thomas VanDrunen and Antony L. Hosking, Purdue University, USA.
  	Increasing the applicability of scalar replacement, 
  	Byoungro So and Mary Hall, University of Southern California, USA.
  	Reducing the cost of object boxing, 
  	Tim Owen and Des Watson, University of Sussex, Brighton, UK.
  	Solving disjunctive/conjunctive boolean equation systems with
  	alternating fixed points
  	Misa Keinänen, Jan Friso Groote, 
  	How Vacuous is Vacuous?
  	Marsha Chechik, Arie Gurfinkel
  	A Temporal Logic of Nested Calls and Returns
  	P. Madhusudan,  Rajeev Alur, Kousha Etessami
  	Liveness with Incomprehensible Ranking
  	Amir Pnueli, Yi Fang, Nir Piterman, Lenore Zuck
  FOSSACS: Analysis of Computation
  	A Denotational Account of Untyped Normalization by Evaluation
  	A. Filinski and H.K. Rohde
  	Hypergraphs and Degrees of Parallelism: A Completeness Result
  	A. Bucciarelli and B. Leperchey
  	Strong normalization of lambda-bar-mu-mu-tilde-calculus with explicit
  	E. Polonovski
  	Soft Lambda-Calculus: A Language for Polynomial Time Computation
  	P. Baillot and V. Mogbil
  12.30 - 14.30: LUNCH
  CC: Code Generation and Backend Optimizations
  	FFT compiler techniques, 
  	Stefan Kral, Franz Franchetti, Juergen Lorenz, Christoph W. Ueberhuber, and 
  	Peter Wurzinger, Vienna University of Technology, Austria.
  	Widening integer arithmetic, 
  	Kevin Redwine and Norman Ramsey, Harvard University, USA.
  	Stochastic bit-width approximation using Extreme Value Theory for customizable processors, 
  	Emre Ozer, Andy P. Nisbet, David Gregg, Trinity College, Dublin, Ireland.
  	Using multiple memory access instructions for reducing code size, 
  	Neil Johnson and Alan Mycroft, University of Cambridge, UK.
  	Guided Invariant Model Checking Based on Abstraction and Symbolic
  	Pattern Databases
  	Kairong Qian, Albert Nymeyer
  	Numerical Domains with Summarized Dimensions
  	Denis Gopan, Frank DiMaio, Nurit Dor, Thomas Reps, Mooly Sagiv
  	Symbolically Computing Most-Precise Abstract Operations for Shape
  	Greta Yorsh, Thomas Reps, Mooly Sagiv
  	Monotonic Abstraction-Refinement for CTL
  	Orna Grumberg, Sharon Shoham
  FOSSACS: Spatial Logics and Game Semantics
  	Decidability of Freshness, Undecidability of Revelation (Extended Abstract)
  	G. Conforti and G. Ghelli
  	Behavioral and Spatial Observations in a Logic for the Pi-Calculus
  	L. Caires
  	Angelic Semantics of Fine-Grained Concurrency
  	D.R. Ghica and A.S. Murawski
  	A Game Semantics of Local Names and Good Variables
  	J. Laird
  16.30 - 17.00: coffee
  CC: Compiler Construction
  	Integrating the Soot compiler infrastructure into an IDE, 
  	Jennifer Lhotak, Ondrej Lhotak, and Laurie Hendren, McGill University, Montreal, Canada.
  	Declarative composition of stack frames, 
  	Christian Lindig, Universitaet Saarbruecken, Germany and Norman Ramsey, Harvard University, USA.
  	Omega-Regular Model Checking
  	Bernard Boigelot, Axel Legay, Pierre Wolper
  	FASTer acceleration of counter automata in practice
  	Bardin, Sebastien
  	Alain Finkel, Jerome Leroux
  	From Complementation to Certification
  	Moshe Vardi, Orna Kupferman 
  FOSSACS: Mobile Calculi
  	SAFEDPI: a language for controlling mobile code (Extended Abstract)
  	M. Hennessy, J. Rathke and N. Yoshida
  	Strong Bisimulation for the Explicit Fusion Calculus
  	L. Wischik and P. Gardner
  	Electoral Systems in Ambient Calculi
  	I. Phillips and M.G. Vigliotti