P. Aziz-abdulla, A. Annichini, and A. Bouajjani, Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol, TACAS '99: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp.208-222, 1999.
DOI : 10.1007/3-540-49059-0_15

P. Aziz-abdulla, A. Bouajjani, and B. Jonsson, On-the-fly analysis of systems with unbounded, lossy FIFO channels, CAV '98: Proceedings of the 10th International Conference on Computer Aided Verification, pp.305-318, 1998.
DOI : 10.1007/BFb0028754

S. Bardin, A. Finkel, J. Leroux, and L. Petrucci, FAST: Fast Acceleration of Symbolic Transition Systems, Proceedings of the 15th International Conference on Computer Aided Verification (CAV'03), volume 2725 of Lecture Notes in Computer Science, pp.118-121, 2003.
DOI : 10.1007/978-3-540-45069-6_12
URL : https://hal.archives-ouvertes.fr/hal-00084185

G. V. Bochmann, Finite state description of communication protocols, Computer Networks (1976), vol.2, issue.4-5, 1995.
DOI : 10.1016/0376-5075(78)90015-6

B. Boigelot and P. Godefroid, Symbolic verification of communication protocols with infinite state spaces using qdds. Form, Formal Methods in System Design, vol.14, issue.3, pp.237-255, 1997.
DOI : 10.1023/A:1008719024240

B. Boigelot, P. Godefroid, B. Willems, and P. Wolper, The power of QDDs (extended abstract), SAS '97: Proceedings of the 4th International Symposium on Static Analysis, pp.172-186, 1997.
DOI : 10.1007/BFb0032741

A. Bouajjani and P. Habermehl, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Theoretical Computer Science, vol.221, issue.1-2, pp.211-250, 1999.
DOI : 10.1016/S0304-3975(99)00033-X

A. Bouajjani, P. Habermehl, and T. Vojnar, Abstract Regular Model Checking, CAV, pp.372-386, 2004.
DOI : 10.1007/978-3-540-27813-9_29
URL : https://hal.archives-ouvertes.fr/hal-00159512

A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili, Regular Model Checking, Computer Aided Verification, pp.403-418, 2000.
DOI : 10.1007/10722167_31
URL : https://hal.archives-ouvertes.fr/hal-00159512

F. Bourdoncle, Sémantiques des Langages Impératifs d'Ordre Supérieur et Interprétation Abstraite, 1992.

D. Brand and P. Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM, vol.30, issue.2, pp.323-342, 1983.
DOI : 10.1145/322374.322380

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, pp.84-96, 1978.
DOI : 10.1145/512760.512770

G. Cécé, A. Finkel, and S. Iyer, Unreliable Channels Are Easier to Verify Than Perfect Channels, Information and Computation, vol.124, issue.1, pp.20-31, 1996.
DOI : 10.1006/inco.1996.0003

A. Deutsch, Interprocedural may-alias analysis for pointers: beyond klimiting, PLDI '94: Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, pp.230-241, 1994.
DOI : 10.1145/178243.178263

J. Feret, Abstract Interpretation-Based Static Analysis of Mobile Ambients, Eighth International Static Analysis Symposium (SAS'01), number 2126 in LNCS, 2001.
DOI : 10.1007/3-540-47764-0_24
URL : https://hal.archives-ouvertes.fr/inria-00527929

A. Finkel, S. P. Iyer, and G. Sutre, Well-abstracted transition systems: application to FIFO automata, Information and Computation, vol.181, issue.1, pp.1-31, 2003.
DOI : 10.1016/S0890-5401(02)00027-5
URL : http://doi.org/10.1016/s0890-5401(02)00027-5

C. Jard and M. , Specification of properties is required to verify distributed algorithms, Colloque AFCET sur les langages de spécification, 1987.

D. Lesens, N. Halbwachs, and P. Raymond, Automatic verification of parameterized linear networks of processes, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.346-357, 1997.
DOI : 10.1145/263699.263747

W. Peng and S. Puroshothaman, Data flow analysis of communicating finite state machines, ACM Transactions on Programming Languages and Systems, vol.13, issue.3, pp.399-442, 1991.
DOI : 10.1145/117009.117015

K. J. Turner, Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL, 1993.

P. Wolper and B. Boigelot, An automata-theoretic approach to presburger arithmetic constraints (extended abstract), SAS '95: Proceedings of the Second International Symposium on Static Analysis, pp.21-32, 1995.
DOI : 10.1007/3-540-60360-3_30
URL : http://orbi.ulg.ac.be/jspui/handle/2268/74877