S. Bardin, A. Finkel, J. Leroux, and L. Petrucci, FAST: Fast Acceleration of Symbolic Transition Systems, Computer Aided Verification (CAV'03), 2003.
DOI : 10.1007/978-3-540-45069-6_12
URL : https://hal.archives-ouvertes.fr/hal-00084185

F. Besson, T. Jensen, D. L. Métayer, and T. Thorn, Model checking security properties of control flow graphs, Journal of Computer Security, vol.9, issue.3, 2001.
DOI : 10.3233/JCS-2001-9303

B. Boigelot and P. Godefroid, Symbolic verification of communication protocols with infinite state spaces using QDDs, Formal Methods in System Design, vol.14, issue.3, 1997.
DOI : 10.1007/3-540-61474-5_53

B. Boigelot, P. Godefroid, B. Willems, and P. Wolper, The power of QDDs (extended abstract), Static Analysis Symposium, SAS'97, 1997.
DOI : 10.1007/BFb0032741

M. Bojanczyk, A. Muscholl, T. Schwentick, L. Segoufin, and C. David, Twovariable logic on words with data, Symposium on Logic in Computer Science,LICS '06, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00151749

A. Bouajjani, J. Esparza, and O. Maler, Reachability analysis of pushdown automata: Application to model-checking, Int. Conf. on Concurrency Theory, CONCUR'97, 1997.
DOI : 10.1007/3-540-63141-0_10

A. Bouajjani and P. Habermehl, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Theoretical Computer Science, vol.221, issue.12, 1999.

A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar, Abstract Regular Tree Model Checking of Complex Dynamic Data Structures, Static Analysis Symposium, SAS'06, 2006.
DOI : 10.1007/11823230_5
URL : https://hal.archives-ouvertes.fr/hal-00150139

M. Bozga, J. Fernandez, L. Ghirvu, C. Jard, T. Jéron et al., Verification and test generation for the SSCOP protocol, Scientific Computer Programming, 2000.
DOI : 10.1016/S0167-6423(99)00017-9

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

A. Janusz and . Brzozowski, Derivatives of regular expressions, J. ACM, vol.11, issue.4, 1964.

D. Caucal, On the regular structure of prefix rewriting, Theoretical Computer Science, vol.106, 1992.

C. Constant, B. Jeannet, and T. Jéron, Automatic Test Generation from Interprocedural Specifications, 2007.
DOI : 10.1007/978-3-540-73066-8_4
URL : https://hal.archives-ouvertes.fr/inria-00137064

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

P. Cousot and R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, Symposium on Programming Language Implementation and Logic Programming, 1992.
DOI : 10.1007/3-540-55844-6_142

D. Distefano, O. Peter, H. Hearn, and . Yang, A Local Shape Analysis Based on Separation Logic, Tools and Algorithms for the Construction and Analysis of Systems, TACAS'06, 2006.
DOI : 10.1145/514188.514190

J. Esparza and J. Knoop, An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis, Int. Conf. on Foundations of Software Science and Computation Structure (FoSSaCS '99), volume 1578 of LNCS, 1999.
DOI : 10.1007/3-540-49019-1_2

J. Esparza and S. Schwoon, A BDD-Based Model Checker for Recursive Programs, Computer Aided Verification, CAV'01, 2001.
DOI : 10.1007/3-540-44585-4_30

J. Feret, Abstract Interpretation-Based Static Analysis of Mobile Ambients, Eighth Int. 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, 2003.
DOI : 10.1016/S0890-5401(02)00027-5
URL : http://doi.org/10.1016/s0890-5401(02)00027-5

A. Finkel, B. Willems, and P. Wolper, A direct symbolic approach to model checking pushdown systems, Electronic Notes on Theoretical Computer Science, vol.9, 1997.

T. L. Gall, B. Jeannet, and T. Jéron, Verification of Communication Protocols Using Abstract Interpretation of FIFO Queues, Algebraic Methodology and Software Technology, AMAST '06, 2006.
DOI : 10.1007/11784180_17

D. Gopan and F. Dimaio, Nurit Dor, Thomas Reps, and Mooly Sagiv Numeric domains with summarized dimensions, Tools and Algorithms for the Construction and Analysis of Systems, TACAS'04, 2004.
DOI : 10.1007/978-3-540-24730-2_38
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.8931

N. Halbwachs, Y. Proy, and P. Roumanoff, Verification of real-time systems using linear relation analysis, Formal Methods in System Design, vol.11, issue.2, 1997.

M. Higuchi, O. Shirakawa, H. Seki, M. Fujii, and T. Kasami, A verification procedure via invariant for extended communicating finite-state machines, Computer Aided Verification,CAV '92, 1993.
DOI : 10.1007/3-540-56496-9_30

B. Jeannet, Dynamic partitioning in linear relation analysis. application to the verification of reactive systems, Formal Methods in System Design, vol.23, issue.1, 2003.

B. Jeannet and W. Serwe, Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs, Int. Conf. on Algebraic Methodology and Software Technology, AMAST'04, 2004.
DOI : 10.1007/978-3-540-27815-3_22
URL : https://hal.archives-ouvertes.fr/inria-00071678

H. Thierry-jéron, V. Marchand, and . Rusu, Symbolic determinisation of extended automata, IFIP Int. Conf. on Theoretical Computer Science, IFIP book series, 2006.

D. Neil, S. S. Jones, and . Muchnick, A flexible approach to interprocedural data flow analysis and programs with recursive data structures, Symposium on Principles of Programming Languages (POPL'82), 1982.

M. Kaminski and N. Francez, Finite-memory automata, Theoretical Computer Science, vol.134, issue.2, 1994.
DOI : 10.1016/0304-3975(94)90242-9
URL : http://doi.org/10.1016/0304-3975(94)90242-9

M. Karr, Affine relationships among variables of a program, Acta Informatica, vol.6, issue.2, 1976.
DOI : 10.1007/BF00268497

D. Lee, K. K. Ramakrishnan, W. M. Moh, and U. Shankar, Protocol specification using parameterized communicating extended finite stte machines -a case study of the atm abr rate control scheme, Int. Conf. on Network Protocols (ICNP '96), 1996.

L. Mauborgne, Representation of sets of trees for abstract interpretation, 1999.

L. Mauborgne, Tree Schemata and Fair Termination, Static Analyis Symposium, SAS'00, 2000.
DOI : 10.1007/978-3-540-45099-3_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.486

L. Mauborgne and X. Rival, Trace Partitioning in Abstract Interpretation Based Static Analyzers, European Symposium on Programming, ESOP'05, 2005.
DOI : 10.1007/978-3-540-31987-0_2

T. Milo, D. Suciu, and V. Vianu, Typechecking for XML transformers, Symposium on Principles of Database Systems, 2000.
DOI : 10.1016/s0022-0000(02)00030-2
URL : http://doi.org/10.1016/s0022-0000(02)00030-2

F. Neven, T. Schwentick, and V. Vianu, Towards Regular Languages over Infinite Alphabets, LNCS, vol.2136, 2001.
DOI : 10.1007/3-540-44683-4_49
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.2304

M. Nielsen, G. Plotkin, and G. Winskel, Petri nets, event structures and domains, part I, Theoretical Computer Science, vol.13, issue.1, 1981.
DOI : 10.1016/0304-3975(81)90112-2
URL : http://doi.org/10.1016/0304-3975(81)90112-2

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

M. Reniers and S. Mauw, High-level message sequence charts, SDL Forum, 1997.

T. Reps, S. Schwoon, S. Jha, and D. Melski, Weighted pushdown systems and their application to interprocedural dataflow analysis, Science of Computer Programming, vol.58, issue.12, 2005.
DOI : 10.1007/3-540-44898-5_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.130.8068

N. Rinetzky and M. Sagiv, Interprocedural Shape Analysis for Recursive Programs, Compiler Construction, CC'01, 2001.
DOI : 10.1007/3-540-45306-7_10
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.1725

V. Rusu, Combining formal verification and conformance testing for validating reactive systems, Software Testing, Verification and Reliability, vol.3, issue.3, 2003.
DOI : 10.1002/stvr.274
URL : https://hal.archives-ouvertes.fr/inria-00527591

M. Sagiv, T. Reps, and R. Wilhelm, Parametric shape analysis via 3-valued logic, Symposium on Principles of Programming Languages (POPL'99), 1999.
DOI : 10.1145/514188.514190
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.3161

M. Sharir and A. Pnueli, Semantic foundations of program analysis, Program Flow Analysis: Theory and Applications, 1981.

T. Yavuz-kahveci and T. Bultan, Automated Verification of Concurrent Linked Lists with Counters, Static Analysis Symposium, SAS'02, 2002.
DOI : 10.1007/3-540-45789-5_8