Publications

This page presents my research papers sorted by year. Ask me for updates on my current work if you are interested.

2008

  • Efficient Static Analysis of XML Paths and Types [inria] [pdf] [bib] new!
    Pierre Genevès and Nabil Layaïda and Alan Schmitt
    INRIA Research Report 6590, July 2008
    Long version of the PLDI'07 paper (includes proofs, crucial implementation techniques for building a satisfiability-testing algorithm which performs well in practice, detailed descriptions of the algorithm, and formal explanations about an important property of the logic: cycle-freeness for formulas).
  • Static Analysis of XML Programs [ercim] [pdf] [bib]
    Pierre Genevès and Nabil Layaïda
    (invited communication) in ERCIM News, number 72: "The Future Web", 2008

2007

  • Efficient Static Analysis of XML Paths and Types [acm] [pdf] [bib]
    Pierre Genevès and Nabil Layaïda and Alan Schmitt
    PLDI'07: the ACM SIGPLAN Conference on Programming Language Design and Implementation (top 0.24% according to Citeseer)
    A new logic for reasoning over finite trees is proposed. This logic currently offers the best balance known between expressivity and complexity for decidability. It is as expressive as monadic second-order logic whereas its satisfiability is shown decidable in time complexity 2^O(n) w.r.t. size n of the formula. We present an effective algorithm in practice using symbolic techniques (BDDs), and use it for the static analysis of XPath queries in the presence of regular tree types, including XPath typing.
  • XPath Typing Using a Modal Logic with Converse for Finite Trees [pdf] [bib]
    Pierre Genevès and Nabil Layaïda and Alan Schmitt
    PLAN-X 2007: the ACM SIGPLAN Workshop on Programming Language Techniques for XML colocated with POPL 2007
    (preliminary version of the above PLDI'07 paper)
  • Deciding XPath Containment with MSO [elsevier] [pdf] [bib]
    Pierre Genevès and Nabil Layaïda
    Data & Knowledge Engineering (DKE), Elsevier, 2007.
    (preliminary version as INRIA Research Report 5867, March 2006 [inria] [pdf] [bib])
    Experiments are conducted with monadic second order logic (using the MONA system) in order to decide containment of XPath queries (e.g. whether or not for all XML trees the result of a regular query is always included in the result of another one).

2006

  • A System for the Static Analysis of XPath [acm] [pdf] [bib]
    Pierre Genevès and Nabil Layaïda
    ACM Transactions on Information Systems (TOIS), Volume 24, Number 4, October 2006
    Major decision problems encountered in the static analysis of XPath (such as query containment, satisfiability, and overlap) are solved in the presence or absence of regular tree type constraints, by reduction to satisfiability of the alternation-free modal μ-calculus over graphs.
  • Comparing XML Path Expressions [acm] [pdf] [slides] [bib]
    Pierre Genevès and Nabil Layaïda
    International ACM Symposium on Document Engineering 2006
    (preliminary version of the above TOIS'06 article)

2005

  • Compiling XPath for Streaming Access Policy [acm] [pdf] [slides] [bib]
    Pierre Genevès and Kristoffer Rose
    International ACM Symposium on Document Engineering 2005
    (preliminary version in the International Workshop on High Performance XML Processing 2004)
    A method for refactoring XPath 1.0 expressions for stream-based evaluation purposes is presented. XPath is compiled into a state-less and forward only subset. This extends the normalization of XPath expressions into the Core language, as described by the W3C formal semantics draft.

2004

  • Logic-Based XPath Optimization [acm] [pdf] [bib]
    Pierre Genevès and Jean-Yves Vion-Dury
    International ACM Symposium on Document Engineering 2004
    (preliminary version in the International Workshop on High Performance XML Processing 2004)
    This paper uses the containment relation over XPath expressions for optimization purposes. A set of rewriting rules is provided in order to eliminate redundancies and contradictions from XPath queries at compile-time.
  • XPath Formal Semantics and Beyond: A Coq-Based Approach [pdf] [bib]
    Pierre Genevès and Jean-Yves Vion-Dury
    International Conference on Theorem Proving in Higher Order Logics 2004, Emerging Trends
    This paper presents the calculus of inductive constructions (and especially the Coq proof assistant) as a framework for dealing with XPath formal semantics. An FO embedding of XPath is presented and its equivalence with XPath denotational semantics is formally proved. This gives a basis for simplifying the development of formal proofs involving XPath.

2003

  • Editing SMIL with Timelines [pdf] [bib]
    Cécile Roisin, Vincent Kober, Vincent Quint, Pierre Genevès, Patrice Navarro
    SMIL Europe Conference 2003
    Visual techniques for editing structured multimedia documents with SMIL and SVG animations are introduced, together with implementations of corresponding authoring systems.

Thesis

  • Logics for XML [pdf] [bib]
    Pierre Genevès
    PhD Thesis, Institut National Polytechnique de Grenoble, December 2006
    This thesis presents a new logic of finite trees adapted for XML, and its application to the static analysis of XML programming languages. The dissertation presents the investigations (using MSO, and the μ-calculus) that finally lead to the design of the logic and its satisfiability-testing algorithm. The dissertation also presents related symbolic techniques used for the solver implementation. This opens the way for a new class of static analyzers (more details).

Patents

  • Optimization of XPath Expressions For Evaluation Upon Streaming XML Data, Kristoffer Rose and Pierre Genevès, IBM Research Patent, #20050257201, May 2004. This patent was awarded an IBM Invention Achievement Award in July 2004.

Essential Literature
(CNRS / LIG | INRIA ) / WAM project