Re: [moca] Model checking (Stochastic)pi-calculus

[GianLuigi Ferrari <giangi@xxxxxxxxxxx>]

Pascal Poizat wrote:
> 
> Hello,
> 
> I am switching from CCS/CSP/LOTOS process algebras to pi-calculus
> (teaching & research).
> Do you know if there exist papers and/or tools on model-checking
> pi-calculus or stochastic pi-calculus ?
> 

In the context of the EU FET project PROFUNDIS we are developing a
semantic-based verification environment for reasoning about
pi-calculus specifications. The prototype implementation of 
the environment provides several facilities (equivalence checking, 
model checking, etc) and can be exercized over the web (the components
of the
environment are web services).

This is the starting point of the enviroment:
http://jordie.di.unipi.it:8080/pweb.
The facilities of the MWB can be exercized from this page.

The model checking facility (HAL) is available here: 
http://matrix.iei.pi.cnr.it/projects/JACK/hal.html

Information about the PROFUNDIS project are available at these sites: 
http://www.it.uu.se/profundis and http://jordie.di.unipi.it:8080/mihda

gianluigi


-- 
====================================================================
Prof. Gianluigi Ferrari    
Dipartimento di Informatica, Via M. Buonarroti 2, 56100
Pisa                
Phone: ++39 050 2212766
Fax: ++39 050 2212726
E-mail: giangi@xxxxxxxxxxx
====================================================================
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html