Prototype announcement: Pi-static analyzer III.

[Jerome Feret <feret@xxxxxxxxxxxxxx>]

Dear all,

I have just finished implementing my last year SAS paper analysis.
This analysis statically infers a sound -- but not complete --
description of the interactions between the agents of a part of 
a system interacting with an unknown context.  (Context behaviour 
is described by using a worst-case semantics.)

The description of these interactions are non-uniform which means that 
recursive instances of processes are distinguished. The prototype allows
in proving for instance that: 
	- in a ring of processes, each process can only be linked either
with  the first process of the ring or with the next process of the ring;
	- in an ftp-server, used by an unbounded client number, 
answer of client queries are returned to correct clients.

The prototype "pi-static analyzer III" is available via the web:

	http://www.di.ens.fr/~feret/prototypes/prototypes.html.en

A short tutorial and few interpreted examples are also given.

Comments are welcomed !!!

					
-------------------------

Jérôme Feret,
Ëcole Normale Supérieure 
Département d'Informatique
45 rue d'Ulm,  
75 230 Paris Cedex 05
01 44 32 37 66
feret@xxxxxx



  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html