Skip to Main content Skip to Navigation
Conference papers

Efficient Static Analysis of XML Paths and Types

Pierre Genevès 1 Nabil Layaïda 2 Alan Schmitt 3 
2 WAM - Web, adaptation and multimedia
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
3 SARDES - System architecture for reflective distributed computing environments
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : We present an algorithm to solve XPath decision problems under regular tree type constraints and show its use to statically typecheck XPath queries. To this end, we prove the decidability of a logic with converse for finite ordered trees whose time complexity is a simple exponential of the size of a formula. The logic corresponds to the alternation free modal mu-calculus without greatest fixpoint, restricted to finite trees, and where formulas are cycle-free. Our proof method is based on two auxiliary results. First, XML regular tree types and XPath expressions have a linear translation to cycle-free formulas. Second, the least and greatest fixpoints are equivalent for finite trees, hence the logic is closed under negation. Building on these results, we describe a practical, effective system for solving the satisfiability of a formula. The system has been experimented with some decision problems such as XPath emptiness, containment, overlap, and coverage, with or without type constraints. The benefit of the approach is that our system can be effectively used in static analyzers for programming languages manipulating both XPath expressions and XML type annotations (as input and output types).
Document type :
Conference papers
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download
Contributor : Alan Schmitt Connect in order to contact the contributor
Submitted on : Thursday, July 15, 2010 - 4:42:39 PM
Last modification on : Sunday, June 26, 2022 - 4:56:27 AM
Long-term archiving on: : Friday, October 22, 2010 - 11:47:58 AM


Files produced by the author(s)




Pierre Genevès, Nabil Layaïda, Alan Schmitt. Efficient Static Analysis of XML Paths and Types. 2007 ACM SIGPLAN conference on Programming language design and implementation, Jun 2007, New York, NY, United States. pp.342--351, ⟨10.1145/1250734.1250773⟩. ⟨inria-00502789⟩



Record views


Files downloads