Pierre Geneves Pierre Genevès

Publications

Below is a searchable list of my publications in reverse chronological order, with links to additional resources such as slides or implementations, when appropriate. Some of my publications are also indexed on DBLP.

Matching entries: 0
settings...
SPARQLGX: Efficient Distributed Evaluation of SPARQL with Apache Spark. Damien Graux, Louis Jachiet, Pierre Genevès and Nabil Layaïda. In Proceedings of the 15th International Semantic Web Conference, 2016 (ISWC'16). new
BibTeX:
@inproceedings{geneves-iswc2016a,
  author = {Damien Graux and Louis Jachiet and Pierre Genevès and Nabil Layaïda},
  title = {SPARQLGX: Efficient Distributed Evaluation of SPARQL with Apache Spark},
  booktitle = {Proceedings of the 15th International Semantic Web Conference},
  year = {2016}
}
SPARQLGX in Action: Efficient Distributed Evaluation of SPARQL with Apache Spark. Damien Graux, Louis Jachiet, Pierre Genevès and Nabil Layaïda. In Proceedings of the 15th International Semantic Web Conference, 2016 (ISWC'16 demo). new
BibTeX:
@inproceedings{geneves-iswc2016b,
  author = {Damien Graux and Louis Jachiet and Pierre Genevès and Nabil Layaïda},
  title = {SPARQLGX in Action: Efficient Distributed Evaluation of SPARQL with Apache Spark},
  booktitle = {Proceedings of the 15th International Semantic Web Conference},
  year = {2016}
}
Smart Trip Alternatives for the Curious. Damien Graux, Pierre Genevès and Nabil Layaïda. In Proceedings of the 15th International Semantic Web Conference, 2016 (ISWC'16 demo). new
BibTeX:
@inproceedings{geneves-iswc2016c,
  author = {Damien Graux and Pierre Genevès and Nabil Layaïda},
  title = {Smart Trip Alternatives for the Curious},
  booktitle = {Proceedings of the 15th International Semantic Web Conference},
  year = {2016}
}
XQuery and Static Typing: Tackling the Problem of Backward Axes. Pierre Genevès and Nils Gesbert. In Proceedings of the 20th ACM SIGPLAN international conference on Functional programming, 2015 (ICFP'15).
Abstract: 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.
BibTeX:
@inproceedings{geneves-icfp2015,
  author = {Pierre Genevès and Nils Gesbert},
  title = {XQuery and Static Typing: Tackling the Problem of Backward Axes},
  booktitle = {Proceedings of the 20th ACM SIGPLAN international conference on Functional programming},
  year = {2015},
  pages = {88--100},
  doi = {10.1145/2784731.2784746}
}
Reasoning with Style. Martí Bosch, Pierre Genevès and Nabil Layaïda. In Proceedings of the 24th International Joint Conference on Artificial Intelligence, 2015 (IJCAI'15).
Abstract: How CSS files can be refactored automatically for speeding up web browsing.
BibTeX:
@inproceedings{geneves-ijcai2015a,
  author = {Martí Bosch and Pierre Genevès and Nabil Layaïda},
  title = {Reasoning with Style},
  booktitle = {Proceedings of the 24th International Joint Conference on Artificial Intelligence},
  year = {2015},
  pages = {2227--2233},
  url = {http://ijcai.org/Abstract/15/315}
}
On Query-Update Independence for SPARQL. Nicola Guido, Pierre Genevès, Nabil Layaïda and Cécile Roisin. In Proceedings of the 24th ACM International on Conference on Information and Knowledge Management, 2015 (CIKM'15).
BibTeX:
@inproceedings{geneves-cikm2015,
  author = {Nicola Guido and Pierre Genevès and Nabil Layaïda and Cécile Roisin},
  title = {On Query-Update Independence for SPARQL},
  booktitle = {Proceedings of the 24th ACM International on Conference on Information and Knowledge Management},
  year = {2015},
  pages = {1675--1678},
  doi = {10.1145/2806416.2806586}
}
Expressive Logical Combinators for Free. Pierre Genevès and Alan Schmitt. In Proceedings of the 24th International Joint Conference on Artificial Intelligence, 2015 (IJCAI'15).
Abstract: Combinators form a succinct and expressive language without increasing complexity.
BibTeX:
@inproceedings{geneves-ijcai2015b,
  author = {Pierre Genevès and Alan Schmitt},
  title = {Expressive Logical Combinators for Free},
  booktitle = {Proceedings of the 24th International Joint Conference on Artificial Intelligence},
  year = {2015},
  pages = {311--317},
  url = {http://ijcai.org/Abstract/15/050}
}
Efficiently Deciding Mu-Calculus with Converse over Finite Trees. Pierre Genevès, Nabil Layaïda, Alan Schmitt and Nils Gesbert. ACM Trans. Comput. Log. Vol. 16(2), 2015 (TOCL'15).
Abstract: A satisfiability solver and some implementation secrets...
BibTeX:
@article{geneves-tocl2015,
  author = {Pierre Genevès and Nabil Layaïda and Alan Schmitt and Nils Gesbert},
  title = {Efficiently Deciding Mu-Calculus with Converse over Finite Trees},
  journal = {ACM Trans. Comput. Log.},
  year = {2015},
  volume = {16},
  number = {2},
  pages = {16},
  doi = {10.1145/2724712}
}
A Logical Approach to Deciding Semantic Subtyping. Nils Gesbert, Pierre Genevès and Nabil Layaïda. ACM Trans. Program. Lang. Syst. Vol. 38(1), 2015 (TOPLAS'15).
BibTeX:
@article{geneves-toplas2015,
  author = {Nils Gesbert and Pierre Genevès and Nabil Layaïda},
  title = {A Logical Approach to Deciding Semantic Subtyping},
  journal = {ACM Trans. Program. Lang. Syst.},
  year = {2015},
  volume = {38},
  number = {1},
  pages = {3},
  url = {http://doi.acm.org/10.1145/2812805},
  doi = {10.1145/2812805}
}
A comparative analysis of attitude estimation for pedestrian navigation with smartphones. Thibaud Michel, Hassen Fourati, Pierre Genevès and Nabil Layaïda. In International Conference on Indoor Positioning and Indoor Navigation, 2015 (IPIN'15).
BibTeX:
@inproceedings{geneves-ipin15,
  author = {Thibaud Michel and Hassen Fourati and Pierre Genevès and Nabil Layaïda},
  title = {A comparative analysis of attitude estimation for pedestrian navigation with smartphones},
  booktitle = {International Conference on Indoor Positioning and Indoor Navigation},
  year = {2015},
  pages = {1--10},
  url = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7346767},
  doi = {10.1109/IPIN.2015.7346767}
}
Static Analysis for Data-Centric Web Programming.. Pierre Genevès. Habilitation Thesis, Université Grenoble Alpes, November, 2014.
Abstract: This document presents an excerpt from the research results that I have obtained since I received a PhD in December 2006. My research addresses one fundamental challenge of our time: building the necessary theoretical foundations and practical tools for ensuring guarantees on web applications such as robustness, security, privacy, and efficiency, towards a web of trust. For this purpose, I build static analysis methods that analyse the source code of web applications for the purpose of automatically detecting defects, or certifying guarantees such as the absence of certain kinds of errors, otherwise. The methods that I develop can also be used for performing semantically-verified optimisations, in compiler design for instance. One particularity of my approach resides in the introduction of novel reasoning techniques, based on new rich modal logics and innovative algorithmic techniques. Another particularity of my research is that it considers theoretical aspects, algorithmic aspects as well as applied aspects such as implementation techniques, experimental validation, and practical relevance. The overall goal of my research is to enable people to construct more reliable, secure, and efficient information systems.
BibTeX:
@phdthesis{geneves-hdr2014,
  author = {Pierre Genevès},
  title = {Static Analysis for Data-Centric Web Programming.},
  school = {Habilitation Thesis, Université Grenoble Alpes},
  year = {2014}
}
Equipping IDEs with XML-Path Reasoning Capabilities. Pierre Genevès and Nabil Layaïda. ACM Trans. Internet Techn. Vol. 13(4), 2014 (TOIT'14).
Abstract: We present the first development environment augmented with static detection of inconsistent XPath expressions for facilitating the development and debugging of web applications.
BibTeX:
@article{geneves-toit2014,
  author = {Pierre Genevès and Nabil Layaïda},
  title = {Equipping IDEs with XML-Path Reasoning Capabilities},
  journal = {ACM Trans. Internet Techn.},
  year = {2014},
  volume = {13},
  number = {4},
  pages = {13:1--13:20},
  doi = {10.1145/2602573}
}
Automated Refactoring for Size Reduction of CSS Style Sheets. Martí Bosch, Pierre Genevès and Nabil Layaïda. In Proceedings of the 2014 ACM symposium on Document engineering, 2014 (DocEng'14).
BibTeX:
@inproceedings{geneves-doceng2014,
  author = {Martí Bosch and Pierre Genevès and Nabil Layaïda},
  title = {Automated Refactoring for Size Reduction of CSS Style Sheets},
  booktitle = {Proceedings of the 2014 ACM symposium on Document engineering},
  year = {2014},
  pages = {13--16}
}
Evaluating and Benchmarking SPARQL Query Containment Solvers. Melisachew W. Chekol, Jérôme Euzenat, Pierre Genevès and Nabil Layada. In Proceedings of the 12th International Semantic Web Conference, 2013 (ISWC'13).
Abstract: We report on deciding SPARQL query containment with state-of-the-art logical solvers. (Nominee for best paper award).
BibTeX:
@inproceedings{geneves-iswc2013,
  author = {Melisachew Wudage Chekol and Jérôme Euzenat and Pierre Genevès and Nabil Layada},
  title = {Evaluating and Benchmarking SPARQL Query Containment Solvers},
  booktitle = {Proceedings of the 12th International Semantic Web Conference},
  year = {2013},
  pages = {408-423},
  url = {http://link.springer.com/chapter/10.1007/978-3-642-41338-4_26}
}
XML Validation: looking backward - strongly typed and flexible XML processing are not incompatible. Pierre Genevès and Nabil Layada. In Proceedings of the 22nd international conference on World Wide Web companion Rio de Janeiro, Brazil, 2013 (WWW'13 poster).
Abstract: XML Schemas and Schematron share the same logical foundations.
BibTeX:
@inproceedings{geneves-www2013,
  author = {Pierre Genevès and Nabil Layada},
  title = {XML Validation: looking backward - strongly typed and flexible XML processing are not incompatible},
  booktitle = {Proceedings of the 22nd international conference on World Wide Web companion},
  year = {2013},
  pages = {219--220}
}
Toward automated schema-directed code revision. Raquel Oliveira, Pierre Genevès and Nabil Layaïda. In Proceedings of the 2012 ACM symposium on Document engineering Paris, France, 2012 (DocEng'12).
BibTeX:
@inproceedings{geneves-doceng2012a,
  author = {Raquel Oliveira and Pierre Genevès and Nabil Layaïda},
  title = {Toward automated schema-directed code revision},
  booktitle = {Proceedings of the 2012 ACM symposium on Document engineering},
  year = {2012},
  pages = {103--106},
  doi = {10.1145/2361354.2361377}
}
On the Analysis of Cascading Style Sheets. Pierre Genevès, Nabil Layaïda and Vincent Quint. In Proceedings of the 21st World Wide Web Conference Lyon, France, April, 2012 (WWW'12).
Abstract: We present a unique method for proving the absence of errors in CSS style sheets.
BibTeX:
@inproceedings{geneves-www2012,
  author = {Pierre Genevès and Nabil Layaïda and Vincent Quint},
  title = {On the Analysis of Cascading Style Sheets},
  booktitle = {Proceedings of the 21st World Wide Web Conference},
  year = {2012},
  pages = {809-818},
  doi = {10.1145/2187836.2187946}
}
XML query-update independence analysis revisited. Muhammad Junedi, Pierre Genevès and Nabil Layaïda. In Proceedings of the 2012 ACM symposium on Document engineering Paris, France, 2012 (DocEng'12).
Abstract: 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.
BibTeX:
@inproceedings{geneves-doceng2012b,
  author = {Muhammad Junedi and Pierre Genevès and Nabil Layaïda},
  title = {XML query-update independence analysis revisited},
  booktitle = {Proceedings of the 2012 ACM symposium on Document engineering},
  year = {2012},
  pages = {95--98},
  url = {http://doi.acm.org/10.1145/2361354.2361375},
  doi = {10.1145/2361354.2361375}
}
SPARQL Query Containment Under SHI Axioms. Melisachew W. Chekol, Jérôme Euzenat, Pierre Genevès and Nabil Layaïda. In Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012 (AAAI'12).
Abstract: A novel and extensible approach to SPARQL query containment in the presence of schemas.
BibTeX:
@inproceedings{geneves-aaai2012,
  author = {Melisachew Wudage Chekol and Jérôme Euzenat and Pierre Genevès and Nabil Layaïda},
  title = {SPARQL Query Containment Under SHI Axioms},
  booktitle = {Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence},
  year = {2012},
  url = {http://www.aaai.org/ocs/index.php/AAAI/AAAI12/paper/view/4924}
}
SPARQL Query Containment under RDFS Entailment Regime. Melisachew W. Chekol, Jérôme Euzenat, Pierre Genevès and Nabil Layaïda. In Proceedings of the 6th International Joint Conference on Automated Reasoning, 2012 (IJCAR'12).
Abstract: We investigate query containment for a (P)SPARQL fragment extended with regular path expressions.
BibTeX:
@inproceedings{geneves-ijcar2012,
  author = {Melisachew Wudage Chekol and Jérôme Euzenat and Pierre Genevès and Nabil Layaïda},
  title = {SPARQL Query Containment under RDFS Entailment Regime},
  booktitle = {Proceedings of the 6th International Joint Conference on Automated Reasoning},
  year = {2012},
  pages = {134-148},
  url = {http://dx.doi.org/10.1007/978-3-642-31365-3_13}
}
Query reasoning on trees with types, interleaving and counting. Everardo Bárcenas, Pierre Genevès, Nabil Layaïda and Alan Schmitt. In Proceedings of the 22nd International Joint Conference on Artificial Intelligence, 2011 (IJCAI'11).
Abstract: 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.
BibTeX:
@inproceedings{geneves-ijcai2011,
  author = {Everardo Bárcenas and Pierre Genevès and Nabil Layaïda and Alan Schmitt},
  title = {Query reasoning on trees with types, interleaving and counting},
  booktitle = {Proceedings of the 22nd International Joint Conference on Artificial Intelligence},
  year = {2011},
  pages = {718-723}
}
Parametric Polymorphism and Semantic Subtyping: the Logical Connection. Nils Gesbert, Pierre Genevès and Nabil Layaïda. In Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, 2011 (ICFP'11).
Abstract: 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.
BibTeX:
@inproceedings{geneves-icfp2011,
  author = {Nils Gesbert and Pierre Genevès and Nabil Layaïda},
  title = {Parametric Polymorphism and Semantic Subtyping: the Logical Connection},
  booktitle = {Proceedings of the 16th ACM SIGPLAN international conference on Functional programming},
  year = {2011},
  pages = {107-116},
  doi = {10.1145/2034773.2034789}
}
Inconsistent path detection for XML IDEs. Pierre Genevès and Nabil Layada. In Proceeding of the 33rd international conference on Software engineering New York, NY, USA ACM, 2011 (ICSE'11).
Abstract: 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.
BibTeX:
@inproceedings{geneves-icse2011,
  author = {Genevès, Pierre and Layada, Nabil},
  title = {Inconsistent path detection for XML IDEs},
  booktitle = {Proceeding of the 33rd international conference on Software engineering},
  publisher = {ACM},
  year = {2011},
  pages = {983--985},
  doi = {10.1145/1985793.1985967}
}
Impact of XML Schema Evolution. Pierre Genevès, Nabil Layada and Vincent Quint. ACM Trans. Internet Technol., July Vol. 11, 2011 (TOIT'11).
Abstract: Effects of XML Schema changes on the validity of documents and on the evaluation of queries are formally investigated.
BibTeX:
@article{geneves-toit2011,
  author = {Genevès, Pierre and Layada, Nabil and Quint, Vincent},
  title = {Impact of XML Schema Evolution},
  journal = {ACM Trans. Internet Technol.},
  year = {2011},
  volume = {11},
  pages = {4:1--4:27},
  doi = {10.1145/1993083.1993087}
}
PSPARQL Query Containment. Melisachew W. Chekol, Jérôme Euzenat, Pierre Genevès and Nabil Layaïda. In Proceedings of the 13th International Symposium on Database Programming Languages, Aug, 2011 (DBPL'11).
Abstract: A method for comparing semantic web queries statically. Superseded by AAAI'12 and IJCAR'12 papers.
BibTeX:
@inproceedings{geneves-dbpl2011,
  author = {Melisachew Wudage Chekol and Jérôme Euzenat and Pierre Genevès and Nabil Layaïda},
  title = {PSPARQL Query Containment},
  booktitle = {Proceedings of the 13th International Symposium on Database Programming Languages},
  year = {2011},
  pages = {8 pages}
}
XML reasoning made practical. Pierre Genevès and Nabil Layada. In Proceedings of the 26th International Conference on Data Engineering IEEE, 2010 (ICDE'10).
Abstract: 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.
BibTeX:
@inproceedings{geneves-icde2010,
  author = {Pierre Genevès and Nabil Layada},
  title = {XML reasoning made practical},
  booktitle = {Proceedings of the 26th International Conference on Data Engineering},
  publisher = {IEEE},
  year = {2010},
  pages = {1169-1172},
  doi = {10.1109/ICDE.2010.5447786}
}
Eliminating dead-code from XQuery programs. Pierre Genevès and Nabil Layaïda. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2 Cape Town, South Africa, 2010 (ICSE'10).
Abstract: An XQuery IDE augmented with static analysis features for identifying and eliminating dead code automatically is introduced.
BibTeX:
@inproceedings{geneves-icse2010,
  author = {Pierre Genevès and Nabil Layaïda},
  title = {Eliminating dead-code from XQuery programs},
  booktitle = {Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2},
  year = {2010},
  pages = {305--306},
  doi = {10.1145/1810295.1810363}
}
Debugging standard document formats. Nabil Layaïda and Pierre Genevès. In Proceedings of the 19th international conference on World wide web Raleigh, North Carolina, USA, 2010 (WWW'10).
Abstract: 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.
BibTeX:
@inproceedings{geneves-www2010,
  author = {Nabil Layaïda and Pierre Genevès},
  title = {Debugging standard document formats},
  booktitle = {Proceedings of the 19th international conference on World wide web},
  year = {2010},
  pages = {1269--1272},
  doi = {10.1145/1772690.1772899}
}
On the analysis of queries with counting constraints. Everardo Bárcenas, Pierre Genevès and Nabil Layada. In Proceedings of the 9th ACM symposium on Document engineering New York, NY, USA, 2009 (DocEng'09).
Abstract: The extension of a tree logic with a counting operator along regular path expressions involving upward and downward recursive navigation is discussed.
BibTeX:
@inproceedings{geneves-doceng2009,
  author = {Everardo Bárcenas and Pierre Genevès and Nabil Layada},
  title = {On the analysis of queries with counting constraints},
  booktitle = {Proceedings of the 9th ACM symposium on Document engineering},
  year = {2009},
  pages = {21--24},
  doi = {10.1145/1600193.1600199}
}
Logics for XML: Reasoning about Trees.. Pierre Genevès. VDM Verlag, 2009.
Abstract: Book with the results presented in my PhD thesis.
BibTeX:
@book{geneves-book2009,
  author = {Pierre Genevès},
  title = {Logics for XML: Reasoning about Trees.},
  publisher = {VDM Verlag},
  year = {2009}
}
Identifying query incompatibilities with evolving XML schemas. Pierre Genevès, Nabil Layada and Vincent Quint. In Proceedings of the 14th ACM SIGPLAN international conference on Functional programming Edinburgh, Scotland, 2009 (ICFP'09).
Abstract: 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.
BibTeX:
@inproceedings{geneves-icfp2009,
  author = {Genevès, Pierre and Layada, Nabil and Quint, Vincent},
  title = {Identifying query incompatibilities with evolving XML schemas},
  booktitle = {Proceedings of the 14th ACM SIGPLAN international conference on Functional programming},
  year = {2009},
  pages = {221--230},
  doi = {10.1145/1596550.1596583}
}
Counting in Trees Along Multidirectional Regular Paths. Everardo Bárcenas, Pierre Genevès and Nabil Layaïda. In Informal Proceedings of the ACM SIGPLAN Workshop on Programming Language Techniques for XML colocated with POPL 2009 Savannah, Georgia, USA, January, 2009 (PLAN-X'09).
BibTeX:
@inproceedings{geneves-planx2009,
  author = {Everardo Bárcenas and Pierre Genevès and Nabil Layaïda},
  title = {Counting in Trees Along Multidirectional Regular Paths},
  booktitle = {Informal Proceedings of the ACM SIGPLAN Workshop on Programming Language Techniques for XML colocated with POPL 2009},
  year = {2009},
  url = {http://hal.inria.fr/inria-00358797/en/}
}
Static Analysis of XML Programs. Pierre Genevès and Nabil Layaïda. Ercim News, January(72) ERCIM, 2008.
Abstract: (Invited communication)
BibTeX:
@article{geneves-en2008,
  author = {Pierre Genevès and Nabil Layaïda},
  title = {Static Analysis of XML Programs},
  journal = {Ercim News},
  publisher = {ERCIM},
  year = {2008},
  number = {72},
  pages = {33--34},
  url = {http://ercim-news.ercim.org/content/view/326/536/}
}
Efficient Static Analysis of XML Paths and Types. Pierre Genevès, Nabil Layaïda and Alan Schmitt. INRIA Research Report, July(6590), 2008.
Abstract: 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). Now superseded by our more recent TOCL'15 article.
BibTeX:
@techreport{geneves-rr2008a,
  author = {Pierre Genevès and Nabil Layaïda and Alan Schmitt},
  title = {Efficient Static Analysis of XML Paths and Types},
  school = {INRIA Research Report},
  year = {2008},
  number = {6590},
  url = {http://hal.inria.fr/inria-00305302/en/}
}
XML Reasoning Solver User Manual. Pierre Genevès and Nabil Layaïda. INRIA Research Report, November(6726), 2008.
Abstract: Documentation for using the XML reasoning solver in practice.
BibTeX:
@techreport{geneves-rr2008b,
  author = {Pierre Genevès and Nabil Layaïda},
  title = {XML Reasoning Solver User Manual},
  school = {INRIA Research Report},
  year = {2008},
  number = {6726},
  url = {http://hal.inria.fr/inria-00339184/en}
}
Efficient Static Analysis of XML Paths and Types. Pierre Genevès, Nabil Layaïda and Alan Schmitt. In Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation San Diego, California, USA, 2007 (PLDI'07).
Abstract: 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.
BibTeX:
@inproceedings{geneves-pldi2007,
  author = {Pierre Genevès and Nabil Layaïda and Alan Schmitt},
  title = {Efficient Static Analysis of XML Paths and Types},
  booktitle = {Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation},
  year = {2007},
  pages = {342--351},
  doi = {10.1145/1250734.1250773}
}
Deciding XPath Containment with MSO. Pierre Genevès and Nabil Layaida. Data & Knowledge Engineering, October Vol. 63(1) Elsevier, 2007 (DKE).
Abstract: 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).
BibTeX:
@article{geneves-dke2007,
  author = {Pierre Genevès and Nabil Layaida},
  title = {Deciding XPath Containment with MSO},
  journal = {Data & Knowledge Engineering},
  publisher = {Elsevier},
  year = {2007},
  volume = {63},
  number = {1},
  pages = {108-136},
  doi = {10.1016/j.datak.2006.11.003}
}
XPath Typing Using a Modal Logic with Converse for Finite Trees . Pierre Genevès, Nabil Layaïda and Alan Schmitt. In Informal Proceedings of the ACM SIGPLAN Workshop on Programming Language Techniques for XML colocated with POPL 2007 Nice, France, January, 2007 (PLAN-X'07).
Abstract: Superseded by the PLDI'07 paper.
BibTeX:
@inproceedings{geneves-planx2007,
  author = {Pierre Genevès and Nabil Layaïda and Alan Schmitt},
  title = {XPath Typing Using a Modal Logic with Converse for Finite Trees },
  booktitle = {Informal Proceedings of the ACM SIGPLAN Workshop on Programming Language Techniques for XML colocated with POPL 2007},
  year = {2007},
  url = {http://wam.inrialpes.fr/publications/2007/geneves-planx07.pdf}
}
Logics for XML. Pierre Genevès. PhD Thesis, Institut National Polytechnique de Grenoble, December, 2006.
Abstract: 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.
BibTeX:
@phdthesis{geneves-2006a,
  author = {Pierre Genevès},
  title = {Logics for XML},
  school = {PhD Thesis, Institut National Polytechnique de Grenoble},
  year = {2006},
  url = {http://wam.inrialpes.fr/publications/2006/geneves-phd.pdf}
}
Comparing XML Path Expressions. Pierre Genevès and Nabil Layaïda. In Proceedings of the 2006 ACM Symposium on Document Engineering Amsterdam, The Netherlands, October, 2006 (DocEng'06).
BibTeX:
@inproceedings{geneves-doceng2006,
  author = {Pierre Genevès and Nabil Layaïda},
  title = {Comparing XML Path Expressions},
  booktitle = {Proceedings of the 2006 ACM Symposium on Document Engineering},
  year = {2006},
  pages = {65-74},
  url = {http://wam.inrialpes.fr/publications/2006/CompXPathExp.pdf}
}
A system for the static analysis of XPath. Pierre Genevès and Nabil Layaïda. ACM Trans. Inf. Syst. Vol. 24(4) ACM Press, 2006 (TOIS'06).
Abstract: 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.
BibTeX:
@article{geneves-tois2006,
  author = {Pierre Genevès and Nabil Layaïda},
  title = {A system for the static analysis of XPath},
  journal = {ACM Trans. Inf. Syst.},
  publisher = {ACM Press},
  year = {2006},
  volume = {24},
  number = {4},
  pages = {475--502},
  doi = {10.1145/1185877.1185882}
}
Compiling XPath for Streaming Access Policy. Pierre Genevès and Kristoffer Rose. In Proceedings of the 2005 ACM symposium on Document engineering New York, NY, USA ACM Press, 2005 (DocEng'05).
Abstract: 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.
BibTeX:
@inproceedings{geneves-doceng2005,
  author = {Pierre Genevès and Kristoffer Rose},
  title = {Compiling XPath for Streaming Access Policy},
  booktitle = {Proceedings of the 2005 ACM symposium on Document engineering},
  publisher = {ACM Press},
  year = {2005},
  pages = {52--54}
}
Logic-based XPath optimization. Pierre Genevès and Jean-Yves Vion-Dury. In Proceedings of the 2004 ACM symposium on Document engineering Milwaukee, Wisconsin, USA, 2004 (DocEng'04).
BibTeX:
@inproceedings{geneves-doceng2004,
  author = {Pierre Genevès and Jean-Yves Vion-Dury},
  title = {Logic-based XPath optimization},
  booktitle = {Proceedings of the 2004 ACM symposium on Document engineering},
  year = {2004},
  pages = {211--219},
  doi = {10.1145/1030397.1030437}
}
Compiling XPath into a State-Less and Forward-Only Subset. Pierre Genevès and Kristoffer Rose. In International Workshop on High Performance XML Processing New York, NY, USA, May, 2004.
Abstract: Superseded by the DocEng'05 paper.
BibTeX:
@inproceedings{geneves-iwhpxp004,
  author = {Pierre Genevès and Kristoffer Rose},
  title = {Compiling XPath into a State-Less and Forward-Only Subset},
  booktitle = {International Workshop on High Performance XML Processing},
  year = {2004}
}
XPath Formal Semantics and Beyond: A Coq-Based Approach . Pierre Genevès and Jean-Yves Vion-Dury. In Emerging Trends Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics Salt Lake City, Utah, United States, August University Of Utah, 2004 (TPHOLs'04).
Abstract: 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.
BibTeX:
@inproceedings{geneves-tphols2004,
  author = {Pierre Genevès and Jean-Yves Vion-Dury},
  title = {XPath Formal Semantics and Beyond: A Coq-Based Approach },
  booktitle = {Emerging Trends Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics},
  publisher = {University Of Utah},
  year = {2004},
  pages = {181-198}
}
Eliminating Context-State from XPath. Pierre Genevès and Kristoffer Rose. , October, 2003 (IBM Research Note).
Abstract: 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.
BibTeX:
@unpublished{geneves-note2003,
  author = {Pierre Genevès and Kristoffer Rose},
  title = {Eliminating Context-State from XPath},
  year = {2003},
  url = {http://wam.inrialpes.fr/publications/2003/xpath-cs-removal.pdf}
}
Editing SMIL with Timelines. Cécile Roisin, Vincent Kober, Vincent Quint, Pierre Genevès and Patrice Navarro. In SMIL Europe Conference, February, 2003.
Abstract: Visual techniques for editing structured multimedia documents with SMIL and SVG animations are introduced, together with implementations of corresponding authoring systems.
BibTeX:
@inproceedings{geneves-sec2003,
  author = {Cécile Roisin and Vincent Kober and Vincent Quint and Pierre Genevès and Patrice Navarro},
  title = {Editing SMIL with Timelines},
  booktitle = {SMIL Europe Conference},
  year = {2003}
}