Programme of Tuesday, April 9

9.00 10.00	ESOP Invited Talk Greg Morrisett (Cornell University, USA) Type Checking Systems Code Session chair:  Daniel Le Métayer
10.00 10.45	Coffee
10.45 12.45	TACAS Software verification Session chair:  Wang Yi Relative Completeness of Abstraction Refinement for Software Model Checking Thomas Ball, Andreas Podelski, Sriram K. Rajamani (Microsoft Research, USA & Max-Planck Institute, D) Towards the Automated Verification of Multithreaded Java Programs Giorgio Delzanno, Jean-Francois Raskin, Laurent Van Begin (Universitá di Genova, I & Université Libre de Bruxelles, B) CLPS-B - A Constraint Solver for B F. Bouquet, Bruno Legeard, Fabien Peureux (Laboratoire d'Informatique Université de Franche-Comté, F) Formal Verification of Functional Properties of an SCR-style Software Requirements Specification using PVS Taeho Kim, David Stringer-Calvert, Sungdeok Cha (KAIST, S Korea & SRI Int., USA)	FASE Tool Demos Session chair:  Peter Mosses The Coordination Development Environment Joăo Gouveia, Georgios Koutsoukos, Michel Wermelinger, Luís Andrade, José Luiz Fiadeiro (Univ. Nova de Lisboa, Portugal) The KeY System: Integrating Object-Oriented Design and Formal Methods Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski (Universität Karlsruhe, Germany and Chalmers University, Gothenburg, Sweden) ObjectCheck: A Model Checking Tool for Executable Object-oriented Software System Designs Fei Xie, Vladimir Levin, James C. Browne (University of Texas, Austin, USA) Demonstration of an Operational Procedure for the Model-Based Testing of CTI Systems Andreas Hagerer, Hardi Hungar, Tiziana Margaria, Oliver Niese, Bernhard Steffen, Hans-Dieter Ide (METAFrame-Technologies GmbH, Dortmund, Germany and University of Dortmund, Germany)	ESOP Program analysis : applications Session chair:  Julia Lawall Tool Support for Improving Test Coverage Susan Horwitz (University of Wisconsin and Gramma Tech, USA) Data Space-Oriented Tiling Mahmut Kandemir (Microsystems Design Lab, USA) Propagation of Roundoff Errors in Finite Precision Computations: a Semantics Approach Matthieu Martel (CEA, F) Asserting the Precision of Floating-Point Computations: a Simple Abstract Interpreter (demo paper) Eric Goubault, Matthieu Martel, Sylvie Putot (CEA, F)	ACL
12.45 14.15	Lunch
14.15 15.15	TACAS Invited Talk Michael Lowry (NASA Ames Research Center) Software Construction and Analysis Tools for Future Space Missions Session chair:  Perdita Stevens
15.15 16.00	Coffee
16.00 17.30	TACAS Infinite-state and parametric systems Session chair:  Bernard Steffen Beyond Parameterized Verification Marco Bozzano, Giorgio Delzanno (Univ. Genova, I) Resource-Constrained Model Checking of Recursive Programs Samik Basu, K. Narayan Kumar, L. Robert Pokorny, C. R. Ramakrishnan (State University New York, USA & Chennai Mathematical Inst., India) Model Checking Large-scale and Parameterized Resource Allocation Systems Allen Emerson, Vineet Kahlon (Univ. of Texas at Austin, USA)	FASE Meta-models Session chair:  Ralf-D. Kutsche (Berlin, Germany) Engineering Modelling Languages: A Precise Meta-Modelling Approach Tony Clark, Andy Evans, Stuart Kent (King's College, London, University of York and University of Kent, United Kingdom) ATOM3: A Tool for Multi-formalism Modelling and Meta-modelling Juan de Lara, Hans Vangheluwe (Universidad Autonoma de Madrid, Spain and McGill University, Montreal, Canada) A Toolbox for Automating Visual Software Engineering Luciano Baresi, Mauro Pezzé (Politecnico di Milano, Italy and Universita degli Studi di Milano, Italy)	ESOP Program analysis : principles Session chair:  David Sands A Modular, Extensible Proof Method for Small-step Flow Analyses Mitchell Wand, Galen B. Williamson (Northeastern University, USA) A Prototype Dependency Calculus Peter Thiemann (University of Freiburg, D) Automatic Complexity Analysis Flemming Nielson, Hanne Riis Nielson, Helmut Seidl  (The Technical University of Denmark, Lyngby, Universität Trier)	ACL
17.30 17.45	Short Break
17.45 18.45	TACAS Tool demo Session chair:  Joost-Pieter Katoen Compositional Verification using SVL Scripts Frédéric Lang (INRIA Rhône-Alpes, F)	FASE Formal Approaches towards UML Session chair:  Martin Grosse-Rhode (Berlin, Germany) Enriching OCL using observational mu-calculus Julian Bradfield, Juliana Küster Filipe, Perdita Stevens (University of Edinburgh, United Kingdom) Formal Verification of UML Statecharts with Real-time Extensions Alexandre David, M. Oliver Möller, Wang Yi (Uppsala University, Sweden and Aarhus University, Denmark)	empty	ACL
18:45 19:30	EASST General Assembly Session chair:
20.00