9:00-10:00 FASE invited lecture Symbiosis of Static Analysis and Program Testing Michal Young (Oregon University, USA)
10:00-10:30 R E F R E S H M E N T S
10:30-12:30 TACAS: State Space Reductions State Class Constructions for Branching Analysis of Time Petri Nets Bernard Berthomieu, Francois Vernadat (LAAS-CNRS, F) Branching Processes of High-Level Petri Nets Victor Khomenko, Maciej Koutny (University of Newcastle, UK) Using Petri Net Invariants in State Space Construction Karsten Schmidt (Humboldt-Universitat zu Berlin, D) Optimistic Synchronization-Based State-Space Reduction Scott Stoller, Ernie Cohen (State University of New York at Stony Brook, USA & Cambridge, UK)	10:30-12:30 ESOP: Types Modeling Web Interactions Paul Graunke (Northeastern University, USA), Robert Bruce Findler (University of Chicago, USA), Shriram Krishnamurthi (Brown University, USA), Matthias Felleisen (Northeastern University, USA) Type Inference for a Distributed Pi-Calculus Cedric Lhoussaine (University of Sussex, UK) Type-Safe Update Programming Martin Erwig, Deling Ren (Oregon State University, USA) Type Error Slicing in Implicitly Typed, Higher-Order Languages Christian Haack, J. B. Wells (Heriot-Watt University, UK)	10:30-12:30 FASE: Formal Verification A Temporal Approach to Specification and Verification of Pointer Data-Structures Marcin Kubica (Warsaw University, PL) A Program Logic for Handling JAVACARD's Transaction Mechanism Bernhard Beckert (Universität Karlsruhe, D), Wojciech Mostowski (Chalmers University of Technology, S) Monad Independent Computational Reasoning in HasCasl Lutz Schröder, Till Mossakowski (University of Bremen, D) Visual Specifications of Policies and their Verification Manuel Koch (Frei Universität Berlin, D), Francesco Parisi-Presicce (Università di Roma, I, and George Mason University, USA)
12:30-14:30 L U N C H   B R E A K
14.30 - 16.00 TACAS: Constraint-Solving and Decision Procedures Checking Properties of Heap-Manipulating Procedures with a Constraint Solver Mandana Vaziri, Daniel Jackson (Massachusetts Institute of Technology, USA) Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic Sergey Berezin, Vijay Ganesh, David L. Dill (Stanford University, USA) Strategies for Combining Decision Procedures Sylvain Conchon, Sava Krstic (Oregon Health & Sciences University, USA)	14.30 - 16.00 ESOP: Techniques & Applications Core Formal Molecular Biology Vincent Danos (CNRS University of Paris 7, F), Cosimo Laneve (University of Bologna, I) Requirements on the Execution of Kahn Process Networks Marc Geilen, Twan Basten (Eindhoven University of Technology, NL) Tagging, Encoding, and Jones Optimality Olivier Danvy (University of Aarhus, DK), Pablo E. Martínez López (UNLP, AR)	14.30 - 16.00 FASE: Model Checking Automatic Model Driven Animation of SCR Specifications Angelo Gargantini, Elvinia Riccobene (Università di Catania, I) Probe Mechanism for Object-Oriented Software Testing Anita Goel, (University of Delhi, IND), S. C. Gupta (National Informatics Center, IND), S. K. Wasan (Jamia Millia Islamia, IND) Model Checking Software via Abstraction of Loop Transitions Natasha Sharygina (Carnegie Mellon University, USA), James C. Browne (The University of Texas, USA)
16:00-16:30 R E F R E S H M E N T S
16.30 - 18.30 TACAS: Testing and Verification Generalized Symbolic Execution for Model Checking and Testing Sarfraz Khurshid, Corina Pasareanu, and Willem Visser (Massachusets Institute of Technology, USA & NASA Ames Research Center, USA) Code-based Test Generation for Validation of Functional Processor Descriptions Fabrice Barray, Philippe Codognet, Daniel Diaz, Henri Michel (ST-Microelectronics, F & University of Paris, F) Tool demo: State Space Visualization Jan Friso Groote, Frank van Ham (Technische Universiteit Eindhoven, NL) Tool demo: Automatic Test Generation with AGATHA Céline Bigot, Alain Faivre, Jean-Pierre Gallois, Arnaud Lapitre, David Lugato, Jean-Yves Pierron, Nicolas Rapin (CEA - SACLAY, DRT/LIST/DTSI/SLA, Gif-sur-Yvette, F) Tool demo: LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios Sebastian Uchitel, Robert Chatley, Jeff Kramer, Jeff Magee (Imperial College, UK)	16.30 - 18.30 ESOP: Reasoning The Rely-Guarantee Method in Isabelle/HOL Leonor Prensa Nieto (INRIA Sophia Antipolis, F) Building Certified Libraries for PCC: Dynamic Storage Allocation Dachuan Yu, Nadeem Hamid, Zhong Shao (Yale University, USA) Finite Differencing of Logical Formulas for Static Analysis Thomas Reps (University of Wisconsin, USA), Mooly Sagiv (Tel-Aviv University, IL), Alexey Loginov (University of Wisconsin, USA) Register Allocation by Proof Transformation Atsushi Ohori (Japan Advanced Institute of Science and Technology, J)	16.30 - 18.30 FASE: Model Integrations and Extensions Integration of Formal Data Types within State Diagrams Christian Attiogbe, Pascal Poizat, Gwen Salaiin (Universite de Nantes, F) Xere: Towards a Natural Interoperability between XML and ER Diagrams G. Della Penna, A. Di Marco, B. Intrigila, I. Melatti, A. Pierantonio (Universita' degli Studi dell'Aquila, I) Detecting Implied Scenarios Analyzing Non-Local Branching Choices Henry Muccini (Università degli Studi dell'Aquila, I) Capturing Overlapping, Triggered and Preemptive Collaborations Using MSCs Ingolf H. Krüger (University of California, San Diego, USA)
18.30 - 18.45 Closing session