Publications
This page presents my research papers sorted by year. Ask me for updates on my current work if you are interested.
2010
- Eliminating Dead-Code from XQuery Programs.In ICSE'10, Proceedings of the ACM/IEEE 32nd International Conference on Software Engineering, May 2010.One of the challenges in web software development is to help achieving a good level of quality in terms of code size and runtime performance, for increasingly popular domain specific languages such as XQuery. We present an IDE equipped with static analysis features for assisting the programmer. These features are capable of identifying and eliminating dead code automatically. The tool is based on newly developed formal programming language verification techniques, which are now mature enough to be introduced in the process of software development. This demo illustrates the operations that can be generalized in the IDEs.
- Debugging Standard Document Formats.In WWW'10, Proceedings of the 19th International Conference on World Wide Web, April 2010.We present a tool for helping XML schema designers to obtain a high quality level for their specifications. The tool allows one to analyze relations between classes of XML documents and formally prove them. For instance, the tool can be used to check forward and backward compatibilities of recommendations. When such a relation does not hold, the tool allows one to identify the reasons and reports detailed counter-examples that exemplify the problem. For this purpose, the tool relies on recent advances in logic-based automated theorem proving techniques that allow for efficient reasoning on very large sets of XML documents. We believe this tool can be of great value for standardization bodies that define specifications using various XML type definition languages (such as W3C specifications), and are concerned with quality assurance for their normative recommendations.
- XML Reasoning Made Practical.In ICDE'10, Proceedings of the 26th IEEE International Conference on Data Engineering, March 2010.We present a tool for the static analysis of XPath queries and XML Schemas. The tool introduces techniques used in the field of verification (such as binary decision diagrams) in order to efficiently solve XPath query satisfiability, containment, and equivalence, in the presence of real-world XML Schemas. The tool can be used in query optimizers, in order to prove soundness of query rewriting. It can also be used in type-checkers and optimizing compilers that need to perform all kinds of compile-time analyses involving XPath queries and XML tree constraints.
2009
- On the Analysis of Queries with Counting Constraints.In DocEng'09: Proceedings of the ACM Symposium on Document Engineering, pages 21-24, ACM, September 2009. [acm]We study the analysis problem of XPath expressions with counting constraints. Such expressions are commonly used in document transformations or programs in which they select portions of documents subject to transformations. We explore how recent results on the static analysis of navigational aspects of XPath can be extended to counting constraints. The static analysis of this combined XPath fragment allows to detect bugs in transformations and to perform many kinds of optimizations of document transformations. More precisely, we study how a logic for finite trees capable of expressing upward and downward recursive navigation, can be equipped with a counting operator along regular path expressions.
- Identifying Query Incompatibilities with Evolving XML Schemas.In ICFP'09, Proceedings of the 2009 ACM SIGPLAN International Conference on Functional Programming, pages 221-230, August 2009. [acm] [pdf] [bib] [slides]This article proposes a predicate language and tool for checking whether schema evolutions require a particular query to be updated. Whenever schema evolutions may induce query malfunctions, the system is able to generate annotated XML documents that exemplify bugs, with the goal of helping the programmer to understand and properly overcome undesired effects of schema evolutions.
- Counting in Trees along Multidirectional Regular Paths.In PLAN-X'09, Proceedings of the ACM SIGPLAN Workshop on Programming Language Techniques for XML, January 2009. [proceedings]We propose a tree logic capable of expressing simple cardinality constraints on the number of nodes selected by an arbitrarily deep regular path with backward navigation. Specifically, a sublogic of the alternation-free μ-calculus with converse for finite trees is extended with a counting operator in order to reason on the cardinality of node sets. Also, we developed a bottom-up tableau-based satisfiability-checking algorithm, which resulted to have the same complexity than the logic without the counting operator: a simple exponential in the size of a formula.
2008
- XML Reasoning Solver User Manual.In INRIA Research Report 6726, November 2008. [inria] [pdf] [bib]Documentation for using the XML reasoning solver in practice.
- Efficient Static Analysis of XML Paths and Types.In INRIA Research Report 6590, July 2008. [inria] [pdf] [bib]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.In ERCIM News, number 72: "The Future Web", 2008. [ercim] [pdf] [bib](invited communication)
2007
- Efficient Static Analysis of XML Paths and Types.In PLDI'07: the ACM SIGPLAN Conference on Programming Language Design and Implementation (top 0.24% according to Citeseer)[acm] [pdf] [bib]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.In PLAN-X'07: the ACM SIGPLAN Workshop on Programming Language Techniques for XML colocated with POPL 2007 [pdf] [bib](preliminary version of the above PLDI'07 paper)
- Deciding XPath Containment with MSO.In Data & Knowledge Engineering (DKE), Elsevier, 2007. [elsevier] [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.In ACM Transactions on Information Systems (TOIS), Volume 24, Number 4, October 2006. [acm] [pdf] [bib]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.In International ACM Symposium on Document Engineering 2006 [acm] [pdf] [slides] [bib](preliminary version of the above TOIS'06 article)
2005
-
Compiling XPath for Streaming Access Policy.In International ACM Symposium on Document Engineering 2005 (preliminary version in the International Workshop on High Performance XML Processing 2004) [acm] [pdf] [slides] [bib]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.In International ACM Symposium on Document Engineering 2004 [acm] [pdf] [bib] (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.In International Conference on Theorem Proving in Higher Order Logics 2004, Emerging Trends [pdf] [bib]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
-
Eliminating Context-State from XPath.Research Note (unpublished manuscript), October 2003. [pdf] [bib]This note explains how we can get rid of XPath context state references (such as position() and last()) by rewriting them into other XPath constructs. This allows implementing XPath evaluators that do not need to maintain any context state information.
-
Editing SMIL with Timelines.In SMIL Europe Conference 2003[pdf] [bib]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.PhD Thesis, Institut National Polytechnique de Grenoble, December 2006. [pdf] [bib]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.
