Publications

Many of my publications are also indexed on DBLP.

2016

  • [ISWC'16] SPARQLGX: Efficient Distributed Evaluation of SPARQL with Apache Spark (to appear)new
    Damien Graux, Louis Jachiet, Pierre Genevès and Nabil Layaïda

2015

  • [ICFP'15] XQuery and Static Typing: Tackling the Problem of Backward Axes pdf [acm] [bib]
    Pierre Genevès, Nils Gesbert.
    A static type-checker for XQuery programs, that improves the XQuery standard type system, by solving the long-standing problem of typing backward axes. The prototype jointly uses two solvers.
  • [IJCAI'15] Reasoning with Style pdf [bib] [slides]
    Martí Bosch, Pierre Genevès, Nabil Layaïda.
    How CSS files can be refactored automatically for speeding up web browsing.
  • [IJCAI'15] Expressive Logical Combinators For Free. pdf [bib] [slides]
    Pierre Genevès, Alan Schmitt.
    Combinators form a succinct and expressive language without increasing complexity.
  • [CIKM'15] On Query-Update Independence for SPARQL pdf [bib]
    Nicola Guido, Pierre Genevès, Nabil Layaïda, Cécile Roisin.
  • [TOPLAS'15] A Logical Approach To Deciding Semantic Subtyping. pdf [bib]
    Nils Gesbert, Pierre Genevès, Nabil Layaïda.
    How subtyping for very expressive types can be solved in EXPTIME by reduction to logical satisfiability.
  • [TOCL'15] Efficiently Deciding μ-calculus with Converse over Finite Trees. pdf [acm] [bib]
    Pierre Genevès, Nabil Layaïda, Alan Schmitt, Nils Gesbert.
    A satisfiability solver and some implementation secrets: try the system online.
  • [IPIN'15] A comparative analysis of attitude estimation for pedestrian navigation with smartphones. pdf [bib]
    Thibaud Michel, Hassen Fourati, Pierre Genevès, Nabil Layaïda.

2014

  • [TOIT'14] Equipping IDEs with XML Path Reasoning Capabilities. pdf [bib]
    Pierre Genevès, Nabil Layaïda.
    We present the first development environment augmented with static detection of inconsistent XPath expressions for facilitating the development and debugging of web applications.
  • [DE'14] Automated Refactoring for Size Reduction of CSS stylesheets. pdf [bib]
    Martí Bosch, Pierre Genevès, Nabil Layaïda.

2013

  • [ISWC'13] Evaluating and Benchmarking SPARQL Query Containment Solvers. pdf [bib]
    Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès, Nabil Layaïda.
    We report on deciding SPARQL query containment with state-of-the-art logical solvers. (Nominee for best paper award).
  • [WWW'13] XML Validation: Looking Backward. pdf[acm] [hal] [bib]
    Pierre Genevès and Nabil Layaïda.
    XML Schemas and Schematron share the same logical foundations.

2012

  • [WWW'12] On the Analysis of Cascading Style Sheets. pdf [pdf] [hal] [bib]
    Pierre Genevès, Nabil Layaïda and Vincent Quint.
    We present a unique method for proving the absence of errors in CSS style sheets.
  • [IJCAR'12] SPARQL Query Containment under RDFS Entailment Regime. pdf [pdf] [hal] [bib]
    Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès, Nabil Layaïda.
    We investigate query containment for a (P)SPARQL fragment extended with regular path expressions.
  • [AAAI'12] SPARQL Query Containment under SHI Axioms. pdf [pdf] [hal] [bib]
    Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès, Nabil Layaïda.
    A novel and extensible approach to SPARQL query containment in the presence of schemas.
  • [DE'12b] Toward automated schema-directed code revision. pdf [acm] [hal] [bib]
    Raquel Oliveira, Pierre Genevès, Nabil Layaïda.
  • [DE'12a] XML Query-Update Independence Analysis Revisited. pdf [acm] [hal] [bib]
    Muhammad Junedi, Pierre Genevès, Nabil Layaïda.
    We revisit Benedikt and Cheney's framework for query-update independence analysis and show that performance can be drastically enhanced using a reduction to mu-calculus satisfiability. Compared to previous works, our approach is (i) more expressive from a theoretical point of view, and (ii) more efficient in practice.

2011

  • [ICFP'11] Parametric Polymorphism and Semantic Subtyping: the Logical Connection. pdf [acm] [hal] [bib]
    Nils Gesbert, Pierre Genevès and Nabil Layaïda.
    We consider a type algebra equipped with recursive, product, function, intersection, union, and complement types together with type variables and universal quantification over them. We consider the subtyping relation recently defined by Castagna and Xu between such type expressions and show how this relation can be decided in EXPTIME, answering an open question.
  • [TOIT'11] Impact of XML Schema Evolution. pdf [acm] [hal] [bib]
    Pierre Genevès, Nabil Layaïda and Vincent Quint.
    Effects of XML Schema changes on the validity of documents and on the evaluation of queries are formally investigated.
  • [IJCAI'11] Query reasoning on trees with types, interleaving and counting. pdf [pdf] [hal] [bib]
    Everardo Barcenas, Pierre Genevès, Nabil Layaïda and Alan Schmitt.
    This paper studies logical satisfiability for a fragment of XPath queries extended with (1) limits on the number of elements satisfying a property (i.e., counting) and (2) unordered elements (interleaving), in the presence of schemas.
  • [ICSE'11] Inconsistent Path Detection for XML IDEs. pdf [acm] [hal] [bib]
    Pierre Genevès and Nabil Layaïda.
    The first IDE for XQuery extended with static detection of inconsistent XPath expressions is introduced for simplifying the development and debugging of any application involving XPath expressions.
  • [DBPL'11] PSPARQL Query Containment. pdf [hal] [bib]
    Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès, Nabil Layaïda.
    A method for comparing semantic web queries statically.

2010

  • [ICSE'10] Eliminating Dead-Code from XQuery Programs. pdf [acm] [hal] [bib]
    Pierre Genevès and Nabil Layaïda.
    An XQuery IDE augmented with static analysis features for identifying and eliminating dead code automatically is introduced.
  • [WWW'10] Debugging Standard Document Formats. pdf [acm] [hal] [bib]
    Nabil Layaïda and Pierre Genevès.
    A tool is presented for checking forward and backward compatibilities of XML Schemas and formally prove them. We believe this 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.
  • [ICDE'10] XML Reasoning Made Practical. pdf [hal] [ieee] [bib]
    Pierre Genevès and Nabil Layaïda.
    A tool for solving XPath query satisfiability, containment, and equivalence, in the presence of real-world XML Schemas is presented. It can be used in query optimizers, type-checkers, and optimizing compilers that need to perform compile-time analyses.

2009

  • [ICFP'09] Identifying Query Incompatibilities with Evolving XML Schemas. pdf [acm] [hal] [bib]
    Pierre Genevès and Nabil Layaïda and Vincent Quint.
    A predicate language and tool are introduced 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.
  • Logics for XML: reasoning about trees. [amazon] [bib]
    Pierre Genevès
    ISBN 978-3639193718. VDM Verlag. September 2009.
    Book with the results presented in my PhD thesis.
  • [DE'09] On the Analysis of Queries with Counting Constraints. pdf [acm] [hal] [bib]
    Everardo Bárcenas, Pierre Genevès, and Nabil Layaïda.
    The extension of a tree logic with a counting operator along regular path expressions involving upward and downward recursive navigation is discussed.
  • [PLAN-X'09] Counting in Trees along Multidirectional Regular Paths. pdf [hal] [proceedings]
    Everardo Bárcenas, Pierre Genevès and Nabil Layaïda.
    (preliminary version of the above DE'09 paper)

2008

  • XML Reasoning Solver User Manual.
    Pierre Genevès and Nabil Layaïda.
    In INRIA Research Report 6726, November 2008. Updated in June 2011. pdf [hal] [bib]
    Documentation for using the XML reasoning solver in practice.
  • Efficient Static Analysis of XML Paths and Types.
    Pierre Genevès and Nabil Layaïda and Alan Schmitt.
    In INRIA Research Report 6590, July 2008. pdf [hal] [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.
    Pierre Genevès and Nabil Layaïda.
    In ERCIM News, number 72: "The Future Web", 2008. pdf [ercim] [bib]
    (invited communication)

2007

  • [PLDI'07] Efficient Static Analysis of XML Paths and Types. pdf [acm] [hal] [bib]
    Pierre Genevès and Nabil Layaïda and Alan Schmitt.
    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.
  • [PLAN-X'07] XPath Typing Using a Modal Logic with Converse for Finite Trees. pdf [hal] [bib]
    Pierre Genevès and Nabil Layaïda and Alan Schmitt.
    (preliminary version of the above PLDI'07 paper)
  • [DKE'07] Deciding XPath Containment with MSO. pdf [elsevier] [hal] [bib]
    Pierre Genevès and Nabil Layaïda.
    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

  • [TOIS'06] A System for the Static Analysis of XPath. pdf [acm] [hal] [bib]
    Pierre Genevès and Nabil Layaïda.
    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.
  • [DE'06] Comparing XML Path Expressions. pdf [acm] [hal] [bib]
    Pierre Genevès and Nabil Layaïda.
    (preliminary version of the above TOIS'06 article)

2005

  • [DE'05] Compiling XPath for Streaming Access Policy. pdf [acm] [hal] [bib] (preliminary version in the International Workshop on High Performance XML Processing 2004)
    Pierre Genevès and Kristoffer Rose.
    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

  • [DE'04] Logic-Based XPath Optimization. pdf [acm] [hal] [bib] (preliminary version in the International Workshop on High Performance XML Processing 2004)
    Pierre Genevès and Jean-Yves Vion-Dury.
    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.
  • [TPHOLs'04] XPath Formal Semantics and Beyond: A Coq-Based Approach. pdf [hal] [bib]
    Pierre Genevès and Jean-Yves Vion-Dury.
    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.
  • Compiling XPath into a State-Less and Forward-Only Subset
    Pierre Genevès and Kristoffer Rose
    International Workshop on High Performance XML Processing 2004 pdf [pdf] [hal] [bib]
    A method for refactoring XPath 1.0 expressions for stream-based evaluation purposes is presented. This extends the normalization of XPath expressions into the Core language, as described by the W3C formal semantics draft.

2003

  • Eliminating Context-State from XPath.
    Pierre Genevès and Kristoffer Rose.
    Research Note (unpublished manuscript), October 2003. pdf [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.
  • [SMIL Europe'03] Editing SMIL with Timelines. pdf [pdf] [bib]
    Cécile Roisin, Vincent Kober, Vincent Quint, Pierre Genevès, Patrice Navarro.
    Visual techniques for editing structured multimedia documents with SMIL and SVG animations are introduced, together with implementations of corresponding authoring systems.

Theses

  • Static Analysis for Data-Centric Web Programming.
    Pierre Genevès.
    HDR, Université Grenoble Alpes, November 2014.
  • Logics for XML.
    Pierre Genevès.
    PhD Thesis, Institut National Polytechnique de Grenoble, December 2006. pdf [pdf] [hal] [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.

LinkedIn Profile