Our apologies if you receive multiple copies of this e-mail. ****************** FIRST CALL FOR PARTICIPATION ******************** Fourth International Symposium on Formal Methods for Components and Objects (FMCO 2005) DATES 1 - 4 November 2005 PLACE CWI, Amsterdam, The Netherlands Registration form and more information at the FMCO site http://fmco.liacs.nl/fmco05.html PRELIMINARY PROGRAM Tuesday November 1st -------------------- SESSION: ALGEBRAIC METHODS 9:00 - 10:00 Keynote: Davide Sangiorgi (University of Bologna, IT) The Bisimulation Proof Method: Enhancements and Challenges Break 10:20 - 11:10 Expressiveness via Leader Election Problems C. Palamidessi (INRIA Futurs Saclay and LIX , FR) Break 11:30 - 12:30 Keynote: Wan Fokkink (Free University, NL) Divide and Congruence Lunch break SESSION: COMPONENT AND SERVICE ORIENTED PROGRAMMING 14:30 - 15:00 Keynote: Kung-Kiu Lau (University of Manchester, UK) Towards a Theory of Software Components Break 15:20 - 16:10 Keynote: Luís Caires (New University of Lisbon, PT) t.b.a. 16:10 - 17:00 Synchronized Hyperedge Replacement as a Model for Service Oriented Computing D. Hirsch (Pisa University, IT) Welcome reception Wednesday November 2nd ---------------------- SESSION: HEAP VERIFICATION 9:30 - 10:30 Keynote: Peter O' Hearn (Queen Mary University of London, UK) Smallfoot: A Tool for Checking Separation Logic Footprint Specifications Break 11:10 - 12:00 Keynote: Joost-Pieter Katoen (RWTH Aachen, DE) Verifying Liveness and Safety of Concurrent Heap-Manipulating Programs Lunch break SESSION: TOOLS 13:30 - 14:30 Keynote: Dennis Dams (Bell Labs, USA) Orion: Building Blocks for Program Analyzers Break 14:50 - 16:00 mCRL2: a language and toolset for behavioural modelling and analysis J.-F. Groote (Technical University Eindhoven, NL) Social event and dinner Thursday Nov 3rd ---------------- SESSION: MODEL CHECKING 9:00 - 10:00 Keynote: Orna Grumberg (Technion, ISR) Abstraction and Refinement in Model Checking Break 10:20 - 11:10 Verification of Evolving Software via Component Substitutability Analysis N. Sinha (Carnegie Mellon University, USA) 11:10 - 12:00 Distributed Analysis of Large Systems L. Brim (University Brno, CZ) Lunch break SPECIAL SESSION 13:30 - 14:30 Keynote: John Reynolds (Carnegie Mellon University, USA) t.b.a. Break SESSION: QUANTITATIVE ANALYSIS 14:50 15:40 Quantitative Aspects of Coordination H. Wiklicky (Imperial College London, UK) 15:40 - 16:30 Partial Order Reduction for Markov Decision Processes C. Baier (Bonn University, DE) Friday Nov 4th -------------- SESSION: ASSERTIONAL METHODS 9:00 - 10:00 Keynote: Arnd Poetzsch-Heffter (University of Kaiserslautern, DE) t.b.a. Break 10:20 - 11:10 Beyond Hoare Logic Assertions: Advanced Specification and Verification with JML and ESC/Java2 J. Kiniry (UCD Dublin, IE) Break 11:30 - 12:30 Keynote: Michael Barnett (Microsoft, USA) t.b.a. Lunch break SESSION: SYSTEM DESIGN 14:00 - 15:00 Keynote: Jan van Schuppen (CWI, NL) Decentralized and Modular Control of Discrete-Event Systems Break 15:20 - 16:10 Formal Development of Critical Systems with UML: Methods and Tools J. Jürjens (Technical University Munich, DE) 16:10 - 17:00 UpSTAIRS with Sequence Diagrams K. Stølen (SINTEF ICT, NO) Farewell drink ORGANIZING COMMITTEE F.S. de Boer (CWI and LIACS-Leiden University) M.M. Bonsangue (LIACS-Leiden University) S. Graf (Verimag) W.P. de Roever (CAU)