N. Alon, T. Milo, F. Neven, D. Suciu, and V. Vianu, XML with data values, Proceedings of the twentieth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems , PODS '01, pp.688-722, 2003.
DOI : 10.1145/375551.375570

M. Arenas, W. Fan, and L. Libkin, On the Complexity of Verifying Consistency of XML Specifications, SIAM Journal on Computing, vol.38, issue.3, pp.841-880, 2008.
DOI : 10.1137/050646895

M. Arenas and L. Libkin, XML data exchange: consistency and query answering, Journal of the ACM, vol.55, issue.2, 2008.

H. Björklund, W. Martens, and T. Schwentick, Optimizing Conjunctive Queries over Trees Using Schema Information, Mathematical Foundations of Computer Science, pp.132-143, 2008.
DOI : 10.1007/978-3-540-85238-4_10

M. Bojanczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin, Two-Variable Logic on Words with Data, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 2011.
DOI : 10.1109/LICS.2006.51

URL : https://hal.archives-ouvertes.fr/hal-00151749

M. Bojanczyk, A. Muscholl, T. Schwentick, and L. Segoufin, Two-variable logic on data trees and XML reasoning, Journal of the ACM, vol.56, issue.3, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00151833

P. Bouyer, A. Petit, and D. And-thérien, An Algebraic Characterization of Data and Timed Languages, pp.248-261, 2001.
DOI : 10.1007/3-540-44685-0_17

D. Calvanese, G. D. Giacomo, M. Lenzerini, and M. Vardi, An Automata-Theoretic Approach to Regular XPath, Database Programming Languages, pp.18-35, 2009.
DOI : 10.1007/3-540-46093-4_3

C. David, L. Libkin, and T. Tan, Efficient reasoning about data trees via integer linear programming, Int. Conf. on Database Theory, 2011.
DOI : 10.1145/1938551.1938558

URL : https://hal.archives-ouvertes.fr/hal-00835833

L. M. De-moura and N. Bjørner, Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.

S. Demri and R. Lazic, Ltl with the freeze quantifier and register automata, ACM Transactions on Computational Logic, vol.10, issue.3, 2009.

W. Fan and L. Libkin, On XML integrity constraints in the presence of dtds, Journal of the ACM, vol.49, issue.3, 2002.

D. Figueira, Satisfiability of downward XPath with data equality tests, Proceedings of the twenty-eighth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, PODS '09, pp.197-206, 2009.
DOI : 10.1145/1559795.1559827

P. Genevés and N. Layaida, A system for the static analysis of XPath, ACM Transactions on Information Systems, vol.24, issue.4, pp.475-502, 2006.
DOI : 10.1145/1185877.1185882

R. Givan, D. A. Mcallester, C. Witty, and D. Kozen, Tarskian Set Constraints, Information and Computation, vol.174, issue.2, pp.105-131, 2002.
DOI : 10.1006/inco.2001.2973

M. Jurdzinski and R. Lazic, Alternation-free modal mu-calculus for data trees, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.131-140, 2007.
DOI : 10.1109/LICS.2007.11

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

M. Kaminski and T. Tan, Tree Automata over Infinite Alphabets, Pillars of Computer Science, pp.386-423, 2008.
DOI : 10.1007/978-3-540-78127-1_21

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

E. Kopczynski and A. W. To, Parikh Images of Grammars: Complexity and Applications, 2010 25th Annual IEEE Symposium on Logic in Computer Science, 2010.
DOI : 10.1109/LICS.2010.21

L. Libkin and C. Sirangelo, Reasoning about XML with temporal logics and automata, Journal of Applied Logic, vol.8, issue.2, pp.210-232, 2010.
DOI : 10.1016/j.jal.2009.09.005

URL : http://doi.org/10.1016/j.jal.2009.09.005

S. Malik and L. Zhang, Boolean satisfiability from theoretical hardness to practical success, Communications of the ACM, vol.52, issue.8, pp.76-82, 2009.
DOI : 10.1145/1536616.1536637

W. Martens, F. Neven, and T. Schwentick, Simple off the shelf abstractions for XML schema, ACM SIGMOD Record, vol.36, issue.3, pp.15-22, 2007.
DOI : 10.1145/1324185.1324188

M. Marx, Conditional XPath, ACM Transactions on Database Systems, vol.30, issue.4, pp.929-959, 2005.
DOI : 10.1145/1114244.1114247

T. Milo, D. Suciu, and V. Vianu, Typechecking for XML transformers, Journal of Computer and System Sciences, vol.66, issue.1, pp.66-97, 2003.
DOI : 10.1016/S0022-0000(02)00030-2

URL : http://doi.org/10.1016/s0022-0000(02)00030-2

F. Neven, Automata, Logic, and XML, Computer Science Logic, pp.2-26, 2002.
DOI : 10.1007/3-540-45793-3_2

F. Neven and T. Schwentick, Query automata over finite trees, Theoretical Computer Science, vol.275, issue.1-2, pp.1-2, 2002.
DOI : 10.1016/S0304-3975(01)00301-2

URL : http://doi.org/10.1016/s0304-3975(01)00301-2

F. Neven, T. Schwentick, and V. Vianu, Finite state machines for strings over infinite alphabets, ACM Transactions on Computational Logic, vol.5, issue.3, pp.403-435, 2004.
DOI : 10.1145/1013560.1013562

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

L. Pacholski and A. Podelski, Set constraints: A pearl in research on constraints, Principles and Practice of Constraint Programming, pp.549-562, 1997.
DOI : 10.1007/BFb0017466

C. Papadimitriou, On the complexity of integer programming, Journal of the ACM, vol.28, issue.4, pp.765-768, 1981.
DOI : 10.1145/322276.322287

A. Robinson and A. Voronkov, Handbook of Automated Reasoning, 2001.

T. Schwentick, XPath query containment, ACM SIGMOD Record, vol.33, issue.1, pp.101-109, 2004.
DOI : 10.1145/974121.974140

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

J. Thatcher, Characterizing derivation trees of context-free grammars through a generalization of finite automata theory, Journal of Computer and System Sciences, vol.1, issue.4, pp.317-322, 1967.
DOI : 10.1016/S0022-0000(67)80022-9

K. Verma, H. Seidl, and T. Schwentick, On the Complexity of Equational Horn Clauses, Conference on Automated Deduction, pp.337-352, 2005.
DOI : 10.1007/11532231_25

V. Vianu, A Web odyssey: from Codd to XML, Symp. on Principles of Database Systems, pp.1-15, 2001.

D. West, Introduction to Graph Theory, 2001.