2nd AND FINAL CALL FOR CONTRIBUTED TALKS AND PARTICIPATION
			=

		Workshop on Modelling and Verification/
		Journees  Modelisation et Verification

		C.I.R.M., Marseille, 16 -- 18 Decembre, 1998

		Official Languages : English and French.

		Important Dates : =

		Propositions of communications	1 december 1998 =

		Workshop			16-18 december 1998 


SCIENTIFIC COMMITEE :

Roberto Amadio, 	Universite de Provence. =

Paul Caspi, 		CNRS (Verimag) Grenoble. =

Pierre Lescanne, 	ENS Lyon. =

Denis Lugiez, 		Universite de Provence. =

Michael Rusinowitch, 	INRIA-Lorraine.

THEMES (non-exclusif list) :

Proof Assistants
Cooperation of proof tools
Case studies
Abstract interpretation methods
Model-checking
Synchronous Models =

Internet Protocols
Infinite State Systemes

INVITED SPEAKERS :

Saddek Bensalem, VERIMAG Grenoble,
Analyse des systemes infinis par abstraction.

Dominique Bolignano, Bull-INRIA Paris =

Model-Checking pour la Verification Formelle de Procoles Cryptographiques=
=2E

Pierre Cregut, 	CNET Lannion =

Modularit=81=E9 dans COQ-UNITY.

Robert De Simone, INRIA Sophia =

Analyse par modeles de processus reactifs.

Claude Jard, CNRS Rennes =

On-the-fly model-checking techniques to generate test cases in
conformance testing.

Pierre Wolper, Universite de Liege
La verification des syst=81=E8mes dont l'espace d'=81=E9tats est infini m=
ais
r=81=E9gulier.


CONTRIBUTED TALKS (Very preliminary and incomplete list! =

Deadline for submission: December 1st.)

Francoise Bellegarde, Universite de Franche-Compte,
Verification de proprietes temporelles de systemes reactifs =

dans le cadre d'une specification par raffinement.

Yves Bertot, INRIA Sophia,
Preuve de correction d'un compilateur pour un langage imp=81=E9ratif
(plus DEMO Coq-Ct).

Frederic Besson, IRISA, Rennes,
L'analyse de relations lineaires pour SIGNAL.

Egon Boerger, Universita` di Pisa,
Operational models for compiler verification.

Paul Caspi, VERIMAG Grenoble,
Handling data-flow programs with PVS.

Alain Finkel, ENS Cachan,
Autour des systemes infinis.

Daniel Hirschkoff, ENPC Paris,
Utilisation des techniques up-to pour la bisimulation dans les
contextes de la preuve automatique et de la v=81=E9rification.

F. Kordon, I. Vernier, Universite Paris 6 =

Experiences d'utilisation d'un Environnement de Genie Logiciel
base sur les reseaux de Petri

Olga Kouchnarenko, Universite de Franche-Comte
Intensional Approaches for Symbolic Methods

Line Jakubiec, Universite de Provence,
Specification et verification de circuits synchrones
dans le calcul des constructions avec types co-inductifs.

Pierre Lescanne, ENS Lyon,
Substitutions explictes avec adresses un modele pour les
implantations de langages.

Antoine Rauzy, Universite de Bordeaux,
Verification d'un calculateur de vol pour Aerospatiale.

Philippe Schnoebelen, ENS Cachan,
Deux approches originales pour la verification des processus PA.

Gregoire Sutre, ENS Cachan,
La verification des automates a file reactifs : un
modele pour les systemes reactifs ecrits en Electre.

Hans Toetenel, Delft University
Modeling and Verification using XTG and PMC

Chris Tofts, Leeds University,
Approximating infinite state probabilistic systems syntactically.


PLACE :

Centre International de =

Rencontres Mathematiques, =

Luminy, Case 916, =

13288 Marseille Cedex 9. =

Tel. 04 91 83 30 00. =

Fax 04 91 41 27 86.

Contact :

	Denis Lugiez, =

	Tel. 04 91 11 36 23. =

	Fax 04 91 11 36 02. =

	CMI (LIM),
	39 rue Joliot-Curie, =

	F-13453, Marseille. =

	lugiez@lim.univ-mrs.fr

PROPOSALS OF COMMUNICATIONS AND DEMONSTRATIONS : =


Participants who wish to present a communication on these
themes are invited to send a title and a short abstract (ASCII or LaTeX)
by e-mail to Roberto Amadio (amadio@lim.univ-mrs.fr) before
december 1 1998.  For demonstrations of software tools contact
Denis Lugiez (lugiez@lim.univ-mrs.fr) before december 1 1998.

ACCOMMODATION :

Participation is limited to 50 people.  Prices of full boarding at
CIRM : room 1 bed 301 FF, room 2 beds 254 FF, room large bed 237 FF.
See http://cirm.univ-mrs.fr for informations concerning location
and transportation. Beware that after 9pm the metro is closed. However
(unfrequent) buses from the center of Marseille to Luminy do run the
whole night.  The workshop starts on Wed 16 at 8.30 am
and is expected to end Fri 18 in the (possibly early) afternoon. =

Participants are expected to arrive not earlier than Tue 15 in the
afternoon (a cold buffet will be served in the evening) and leave not
later than Sat 19 in the morning.


GENERAL PRESENTATION :

This workshop is devoted to the mathematical techniques for
the specification an verification of complex software and
hardware systems and their applications.
The proof of circuits, programs, and communication protocols is a
strategic domain. An important issue is to go from the
verification of finite state systems to that of infinite state
systems. Such systems are frequently met: programs with infinite
data structures, parametric systems, with infinite control, with
arbitrary network topologies,... The formal verification of these
systems requires the development of new techniques.

The goal of the Workshop is to present the state of the art in
different approaches to these questions. In particular, we will
consider extensions of model-checking to infinite state systems, proof
assistants and their cooperation with model-checkers, and methods
based on abstraction.

Our aim is to compare the different approaches and to encourage the
exchanges among the practitioners of the different methodologies. We
are also interested in significant case studies in the following
domains: synchronous systems and analysis of Internet protocols, e.g.,
routing protocols, authentication protocols,...