Proofs systems

Ferrari Ferro, Gnesi, Montanari, and Pistore, developed an automata-based verification environment for the $\pi$-calculus. The environment takes a direct advantage of a general theory which allows to associate ordinary finite state automata to a wide class of $\pi$-calculus agents, so that equivalent automata are associated to equivalent agents. A key feature of the approach is the re-use of efficient algorithms and verification techniques (equivalence checkers and model checkers) which have been developed and implemented for ordinary automata. The verification environment has been implemented on top of an existing verification environment for process calculi: the JACK environment.

CNET is also involved in adapting the Coq theorem prover to specify and prove safety and liveness properties of protocols and of distributed algorithms in a modular way. This works implements results already obtained in 1996 by Crégut and Heyd with the theory of Unity. In order to apply Coq-Unity to real-world protocol, a translation from SDL is used. This method is currently applied on an ATM protocol, and is research in progress.