AMAST Mail 1996
[Prev][Next][Index]

School on Verification of Infinite State Systems


        Grenoble-Alpe d'Huez European School of Computer Science

     METHODS AND TOOLS FOR THE VERIFICATION OF INFINITE STATE SYSTEMS

                    Grenoble, March 23-25, 1997


Aim and Scope
-------------

The aim of this school is to assemble researchers and graduate students 
interested in the verification of infinite state systems.

In the last few years many different approaches to this problem have
emerged. The purpose of the school is to give an overview of the state of
the art of current research directions, especially focusing on:

- Results concerning models and verification methods for systems having a
dense state space,   such as real-time and hybrid systems, as well as for
systems with an infinite but discrete state space, such as Petri Nets and
automata extended with unbounded data domains (queues, counters, ...).

- Current trends on the development of verification methods and tools
seeking the extension and the combination of algorithmic and deductive
analysis techniques looking for trade-offs between efficiency and
generality.

The meeting will put special emphasis on the interaction between the
different approaches and on the unification of these frameworks.

The school is organized by VERIMAG and sponsored by the Institut d'Etudes 
Scientifiques Avancees (IESA) of Grenoble. It will take place immediately 
before the International Workshop on Hybrid and Real-Time Systems HART'97.


Invited Speakers
----------------

P. Abdulla (Uppsala, Sweden)
"Model- checking through constraint solving"

R. Alur (Berkeley, USA)
"Compositional reasoning for timed systems"

J. Esparza (Munich, Germany)
"Decidability and complexity of model-checking problems for  
infinite-state systems"

A. Finkel (ENS Cachan, France) 
"Algorithms and semi-algorithms for infinite state systems"

T. Henzinger (Berkeley, USA)
"Some lessons from the HyTech experience"

J. Hooman (Eindhoven, The Netherlands) 
"Verifying distributed real-time systems with PVS"

N. Lynch (MIT, USA)
"On decomposing probabilistic systems"

Z. Manna (Stanford, USA)
"Deductive model-checking"

F. Moller (Uppsala, Sweden)
"Equivalence checking of infinite state automata"

A. Pnueli (Weizmann, Israel)
"Symbolic model-checking with rich assertional languages"

N. Shankar (SRI, USA)
"The use of decision procedures in deductive verification"

B. Steffen (Passau, Germany)
"Second-order model-checking"

P. Wolper (Liege, Belgium)
"A unifying approach to exploring infinite state spaces"


Organizing Committee
--------------------

S. Bensalem (Verimag), A. Bouajjani (Verimag), S. Graf (Verimag), 
Y. Lakhnech (Kiel), S. Yovine (Verimag).


Information and Registration
----------------------------

Information about the venue, registration fees and accommodation, as well as the 
registration form, can be obtained from the school's web page accessible through 
VERIMAG's home page

         http://www.imag.fr/VERIMAG

or by sending e-mail to

         Chantal.Costes@imag.fr

To register, please send the registration form by e-mail to the address above. 
We strongly encourage to register before December 10, 1996.

-----------------------------------------------------------------------------
****************************  INFORMATION ***********************************
-----------------------------------------------------------------------------

Venue
-----

The school takes place in Grenoble at the  MAISON JEAN KUNTZMAN  situated
in the  University campus.

Grenoble, the Capital of the Alpes, is an important information technology
center with  3 universities, 7  schools of engineering, many research
centers such as CNRS, INRIA and CENG, and computer manufacturers, such as
Bull, Schneider Electric and HP, and about 300 software companies.


Travel Information
------------------

By train
-From Paris, (TGV 3 hours and a half).

By plane
-From Grenoble Airport (Saint Geoirs) you have  a bus to  Grenoble (30mn).
Lyon Airport (Satolas)  and  Geneva Airport (Cointrin) are served by most
major airlines. From Satolas you can take a bus to Grenoble (one hour), from
Cointrin  you can take a train to Grenoble (3 hours).


Accommodation
-------------

We propose three hotels in downtown  Grenoble. All the rooms are
sound-proofed, with bathroom, toilet, direct telephone and television. 
The University campus is accessible by tramway (20mn).

GRAND HOTEL ***, is near Grenoble's old town.

Single room   323 FF
Double room   406 FF

HOTEL DES ALPES ** or HOTEL BASTILLE ** are near the railway station.

Single room   242 FF
Double room   334 FF

All the prices include breakfast


Registration fees
-----------------

Before December 10, 1996 :      1500 FF
After  December 10, 1996 :      1700 FF

They include attendance to all sessions, a copy of proceedings, 
banquet, lunches and coffee breaks.


-----------------------------------------------------------------------------
************************* REGISTRATION FORM *********************************
-----------------------------------------------------------------------------

       Grenoble-Alpe d'Huez European School of Computer Science

   METHODS AND TOOLS FOR THE VERIFICATION OF INFINITE STATE SYSTEMS

                      Grenoble, March 23-25, 1997


Name(s) :...........................................
Surname :...........................................
Affiliation :.......................................
Mailing address :...................................
....................................................
....................................................
Phone number :......................................
Fax number :........................................
E. mail : ..........................................
Arrival Date :...................................... 	
First meal :........................................
Departure Date :....................................    
Last meal :.........................................

Please make the following arrangements :
      	
HOTEL       Single Room           Double Room

SAVOIE       323 FF......          406 FF......	

ALPES        242 FF......          334 FF......

BASTILLE     242 FF......          334 FF......

REGISTRATION FEES

Before December 10, 1996           1500 FF......
After  December 10, 1996           1700 FF......

PAYMENT : Indicate which of the following means of payment you will use:

... by cheque to: 
 Monsieur l'Agent Comptable de l'Universite Joseph Fourier, Grenoble I

by bank transfer to:
 ... CCP GRENOBLE 20041 01017 05400 08 Y 028 78
 or
 ... TRESOR PUBLIQUE GRENOBLE 10071 38000 0000300014240


Signature :


Please return this form by e-mail to

       Chantal.Costes@imag.fr

WE STRONGLY ENCOURAGE TO REGISTER BEFORE **** DECEMBER 10, 1996 ****
[ AMAST Mail 1996 | Latest Update | AMAST Mail Meta-Index | AMAST ]