Call for Participation: 7th ERCIM FMICS (Malaga, Spain) July 12-13, 2002

[Hubert Garavel]

******************************************************************************
*
*                         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)
_____________________________________________________________________________