9:00-10:00 ESOP invited lecture What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis Catherine Meadows (Naval Research Laboratory, USA)
10:00-10:30 R E F R E S H M E N T S
10:30-12:30 TACAS: Modules and Compositional Verification Compositional Analysis for Verification of Parameterized Systems Samik Basu, C.R. Ramakrishnan (SUNY at Stony Brook, USA) Learning Assumptions for Compositional Verification Jamieson M. Cobleigh, Dimitra Giannakopoulou, Corina S. Pasareanu (University of Massachusets, USA & NASA Ames Research Center, USA) Automated Module Composition Stavros Tripakis (VERIMAG, F) Modular Strategies for Recursive Game Graphs Rajeev Alur, Salvatore La Torre, P. Madhusudan (University of Pennsylvania, USA & University of Salerno, I)	10:30-12:30 ESOP: Security 1 Security Properties: Two Agents Are Sufficient Hubert Comon-Lundh and Veronique Cortier (LSV, ENS Cachan and CNRS, F) A Simple Language for Real-time Cryptographic Protocol Analysis Roberto Gorrieri, Enrico Locatelli (University of Bologna, I), Fabio Martinelli (IIT-CNR, I) Rule Formats for Non Interference Simone Tini (Universita dell'Insubria, I) On the Secure Implementation of Security Protocols Pablo Giambiagi, Mads Dam (Swedish Institute of Computer Science, S)	10:30-12:30 FASE: Aspect and Object Oriented Programming Towards UML-based Formal Specifications of Component Based Real-Time Software Vieri Del Bianco, Luigi Lavazza (Politecnico di Milano and CEFRIEL, I), Marco Mauri, Giuseppe Occorso (Politecnico di Milano, I) Modelling Recursive Calls with UML State Diagrams Jennifer Tenzer, Perdita Stevens (University of Edinburgh, UK) Pipa: A Behavioral Specification Language for AspectJ Jianjun Zhao, Martin Rinard (Massachusetts Institute of Technology, USA) Tool demo: PacoSuite & JAsCo: A Visual Component Composition Environment with Advanced Aspect Separation Features Wim Vanderperren, Davy Suvée, Bart Wydaeghe (Vrije Universiteit Brussel, B)
12:30-13:30 E A S S T  G e n e r a l  A s s e m b l y
12:30-14:30 L U N C H   B R E A K
14.30 - 15.30 TACAS invited lecture What Are We Trying to Prove? Lessons from our Experiences with Proof-Carrying Code Peter Lee (Carnegie Mellon University, USA)
15.45 - 16.45 TACAS: Symbolic State Spaces and Decision Diagrams Saturation Unbound Gianfranco Ciardo, Robert Marmorstein, Radu Siminiceanu (College of William and Mary, USA) Construction of Efficient BDDs for Bounded Arithmetic Constraints Constantinos Bartzis, Tevfik Bultan (University of California, USA)	15.45 - 16.45 ESOP: Security 2 Handling Encryption in an Analysis for Secure Information Flow Peeter Laud (Tartu University and Cybernetica AS, EST) Using Controller Synthesis to Build Property-Enforcing Layers Karine Altisen (VERIMAG/INPG, F), Aurelie Clodic (LAAS/CNRS, F), Florence Maraninchi (VERIMAG/INPG, F), Eric Rutten (INRIA Rhone-Alpes, F)	15.45 - 16.45 FASE: Distributed and Web Applications Model-Based Development of Web Applications Using Graphical Reaction Rules Reiko Heckel, Marc Lohmann (University of Paderborn, D) Modular Analysis of Dataflow Process Networks Yan Jin, Robert Esser, Charles Lakos (Adelaide University, USA), Jörn W. Janneck (University of California at Berkeley, USA)
16:45-17:15 R E F R E S H M E N T S
17.15 - 18.45 TACAS: Performance and Mobility Modeling and Analysis of Power-Aware Systems Kyriakos Christou, Insup Lee, Anna Philippou, Oleg Sokolsky (University of Pennsylvania, USA & University of Cyprus, CY) Tool demo: A Set of Performance and Dependability Analysis Components for CADP Holger Hermanns, Christophe Joubert (INRIA Rhone-Alpes, Montbonnot Saint-Martin, F) Tool demo: The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems Dezhuang Zhang, Rance Cleaveland, Eugene Stark (State University of New York at Stony Brook, USA) Tool demo: BANANA: A Tool for Boundary Ambients Nesting ANAlysis Chiara Braghin, Agostino Cortesi, Stefano Filippone, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza (University de Venezia, I)	17.15 - 18.45 ESOP: Program Correctness Automatic Software Model Checking using CLP Cormac Flanagan (Systems Research Center, Hewlett Packard, USA) Verifying Temporal Heap Properties Specified via Evolution Logic Eran Yahav (Tel Aviv University, IL), Thomas Reps (University of Wisconsin, USA), Mooly Sagiv (Tel Aviv University, IL), Reinhard Wilhelm (Universitat des Saarlandes, D) Correctness of Data Representations Involving Heap Data Structures Uday Reddy (University of Birmingham, UK), Hongseok Yang (Korean Advanced Institute of Science and Technology, Korea)	17.15 - 18.45 FASE: Sofware Measurements Foundations of a Weak Measurement-Theoretic Approach to Software Measurement Sandro Morasca (Università degli Studi dell'Insubria, I) An Information-Based View of Representational Coupling in Object-Oriented Systems Pierre Kelsen (Luxembourg University of Applied Sciences, L)