****************************************************************************** * * CALL FOR PARTICIPATION * * 7th International Workshop on Formal Methods for Industrial Critical Systems * (FMICS 02) * * University of Málaga (Spain) * July 12-13, 2002 * Colocated with the 29th ICALP conference * * http://www.inrialpes.fr/vasy/fmics/workshop-7 * ****************************************************************************** *** SCOPE OF THE WORKSHOP *** The aim of the FMICS workshops is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, these workshops should bring together scientists who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. They also aim at the promotion of research and development for the improvement of formal methods and tools for industrial applications. *** INVITED SPEAKERS *** Andrew Gordon (Microsoft Research Cambridge, UK) Andreas Podelski Max-Planck Institut für Informatik, Germany) Wang Yi (Uppsala University, Sweden) *** PROGRAMME *** ------------------------ FRIDAY 12 July 2002 --------------------------------- INVITED PRESENTATION Andreas Podelski (Max-Planck Institut für Informatik, Germany) Abstraction for Software Model-Checking SESSION - ABSTRACTION AND MODEL-CHECKING - Chair: H. Garavel (INRIA, France) M. Bourahla (Univ. of Biskra, Algeria), M. Benmohamed (Univ. of Constantine, Algeria) Predicate Abstraction and Refinement for Model Checking VHDL State Machines M. del Mar Gallardo, J. Martinez, P. Merino, E. Pimentel (Univ. of Málaga, Spain) A Tool for Abstraction in Model Checking SESSION - TESTING - Chair: R. Cleaveland (SUNY, New York, USA) D. Lugato, C. Bigot, Y. Valot (CEA Saclay, France) Validation and Automatic Test Generation on UML Models: the AGATHA approach J.C. Burguillo, M. Llamas, M.J. Fernández (Univ. of Vigo, Spain), T. Robles (Polytechnical Univ. of Madrid, Spain) Heuristic-Driven Techniques for Testing Distributed Systems B. Steffen (Univ. of Dortmund, Germany), T. Margaria (METAFrame, Germany), O.Niese (Univ. of Dortmund, Germany) Scalable System-level CTI Testing through Lightweight Coarse-grained Coordination INVITED PRESENTATION Andrew D. Gordon (Microsoft Research, Cambridge, UK) Authenticity Types for Cryptographic Protocols SESSION - INDUSTRIAL CASE STUDIES I - Chair: H. Hermanns (Univ. of Twente, NL) N. Lopez, M. Simonot, V. Donzeau-Gouge (CNAM, Paris, France) A Methodological Process for the Design of a Large System: Two Industrial Case-Studies C. Daws (CWI, Amsterdam, NL), M. Kwiatkowska, G. Norman (Univ. of Birmingham, UK) Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM TOOL DEMOS WORKSHOP BANQUET ----------------------- SATURDAY 12 July 2002 ------------------------------- INVITED PRESENTATION Wang Yi (Uppsala Univ., Sweden) Synthesis of Verified Real Time Software SESSION - INDUSTRIAL CASE STUDIES II - Chair: W. Fokkink (CWI, Amsterdam, NL) V. Valero, F.L. Pelayo, F. Cuartero, D. Cazorla (Univ. of Castilla, Spain) Specification and Analysis of the MPEG-2 Video Encoder with Timed-Arc Petri Nets S. Boldo, M. Daumas (Ecole Normale Supérieure de Lyon, France) Properties of the Subtraction Valid for any Floating Point System SESSION - MODEL CHECKING Chair: S. Gnesi (IEI-CNR, Pisa, Italy) X. Thirioux (IRIT-LIMA, Toulouse, France) Simple and Efficient Translation from LTL Formulas to Buchi Automata A. Biere, C. Artho, V. Schuppan (ETH Zürich, Switzerland) Liveness Checking as Safety Checking H. Hansen (Tempere Univ. of Technology, Finland), W. Penczek (Institute of Computer Science, Warsaw, Poland), A. Valmari (Tempere Univ. of Technology) Stuttering-Insensitive Automata for On-the-Fly Detection of Livelock Properties A.Valmari, H. Virtanen, A. Puhakka (Tempere Univ. of Technology, Finland) Context-Sensitive Visibility FMICS WORKING GROUP MEETING ----------------------------------------------------------------------------- *** REGISTRATION **** The registration procedure is described on the FMICS 02 web site http://www.inrialpes.fr/vasy/fmics/workshop-7 which also provides traveling and accomodation information. *** ORGANIZATION *** FMICS 02 Programme Committee Chairs H. Garavel (INRIA Rhone-Alpes, France) R. Cleaveland (SUNY, New York, USA) FMICS 02 Local Organizing Committee (University of Málaga) M. del Mar Gallardo P. López J. Martínez P. Merino (local organization chair) _____________________________________________________________________________