6 Conclusion
We have implemented the analyses proposed in [5, 6]. The prototype has successfully prove integrity, non-exhaustion of resource and discover mutual exclusion in our both example: the token-ring and a ftp-server. Our analyses are very likely to be extended with other abstract domains and other analyses.
Our framework is very likely to be used in abstracting the mobility
aspect in a programming language such as Erlang the communication mechanism of which is built upon the p-calculus.