Selected Publications (Since 2007)

Titre

Rigid Tree Automata and Applications

Auteurs

Florent Jacquemard; Francis Klay; Camille Vacher

Détail

Information and Computation, Elsevier, 2011, 209 (3), pp. 486-512

DOI

DOI : 10.1016/j.ic.2010.11.015

Début du résumé

We introduce the class of Rigid Tree Automata (RTA), an extension of standard bottom-up automata on ranked trees with distinguished states called rigid. Rigid states define a restriction on the computation of RTA on trees: RTA can test for equality in subtrees reaching the same rigid state. RTA are able to perform local and global tests of equality between subtrees, non-linear tree pattern matching, and some inequality and disequality tests as well. Properties like determinism, pumping lemma, Boolean closure, and several decision problems are studied in detail. In particular, the emptiness problem is shown decidable in linear time for RTA .....

Accès au texte intégral et bibtex

Titre

Sufficient Completeness Verification for Conditional and Constrained Term Rewriting Systems

Auteurs

Adel Bouhoula; Florent Jacquemard

Détail

Journal of Applied Logic, Elsevier, 2011

DOI

DOI : 10.1016/j.jal.2011.09.001

Début du résumé

We present a procedure for checking sufficient completeness of conditional and constrained term rewriting systems containing axioms for constructors which may be constrained (by e.g. equalities, disequalities, ordering, membership...). Such axioms allow to specify complex data structures like e.g. sets, sorted lists or powerlists. Our approach is integrated into a framework for inductive theorem proving based on tree grammars with constraints, a formalism which permits an exact representation of languages of ground constructor terms in normal form. The procedure is presented by an inference system which is shown sound and complete. A precondition of one inference of this system refers .....

Accès au texte intégral et bibtex

Titre

Formalisation des relations temporelles dans un contexte d'accompagnement musical automatique

Auteurs

José Echeveste; Arshia Cont; Jean-Louis Giavitto; Florent Jacquemard

Détail

Hermès. 8e Colloque sur la Modélisation des Systèmes Réactifs (MSR'11), Nov 2011, Lille, France. Modélisation des Systèmes Réactifs : MSR 2011, 45, pp. 109-124, n° spécial du Journal Européen des Systèmes Automatisés (JESA)

Début du résumé

We sketch the real-time features required by automatic musical accompaniment seen as a reactive system. We formalize the datation of musical event taking into account the various temporal scales used in music. Various strategies for the handling of synchronization constraints and the handling of errors are presented. .....

Accès au texte intégral et bibtex

Titre

Controlled Term Rewriting

Auteurs

Florent Jacquemard; Yoshiharu Kojima; Masahiko Sakai

Détail

C. Tinelli and V. Sofronie-Stokkermans. 8th International Symposium Frontiers of Combining Systems (FroCoS 2011), Oct 2011, Saarbrücken, Germany. Springer, Proceedings of the 8th International Symposium Frontiers of Combining Systems (FroCoS), 6989, pp. 179-194, Lecture Notes in Artificial Intelligence

Début du résumé

Motivated by the problem of verification of imperative tree transformation programs, we study the combination, called controlled term rewriting systems (CntTRS), of term rewriting rules with con- straints selecting the possible rewrite positions. These constraints are specified, for each rewrite rule, by a selection automaton which defines a set of positions in a term based on tree automata computations. We show that reachability is PSPACE-complete for so-called monotonic CntTRS, such that the size of every left-hand-side of every rewrite rule is larger or equal to the size of the corresponding right-hand-side, and also for the class of context-free non-collapsing CntTRS, .....

Accès au texte intégral et bibtex

Titre

Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus

Auteurs

Florent Jacquemard; Etienne Lozes; Ralf Treinen; Jules Villard

Détail

Theory of Security and Applications (TOSCA, affiliated to ETAPS), Mar 2011, Saarbrücken, Germany. Springer, Lecture Notes in Computer Science

Début du résumé

We investigate the problem of deciding first-order theories of finite trees with several distinguished congruence relations, each of them given by some equational axioms. We give an automata-based solution for the case where the different equational axiom systems are linear and variable-disjoint (this includes the case where all axioms are ground), and where the logic does not permit to express tree relations x=f(y,z). We show that the problem is undecidable when these restrictions are relaxed. As motivation and application, we show how to translate the model-checking problem of Apil, a spatial equational logic for the applied pi-calculus, to the validity .....

Accès au texte intégral et bibtex

Titre

Modèles d'automates d'arbres étendus pour la vérification de systèmes infinis

Auteurs

Florent Jacquemard

Détail

École normale supérieure de Cachan - ENS Cachan, Nov. 2011. English

Début du résumé

Ce document présente l'étude de plusieurs modèles de machines à états finis qui étendent tous le même formalisme: les automates d'arbres classiques, et leur application dans différentes tâches telles que l'analyse statique de programmes ou de systèmes, la typage, la vérification de la cohérence de spécifications, le model checking... Les arbres sont une structure naturelle de données, très répandue en informatique, par exemple pour la représentation des structures de données hiérarchiques ou imbriquées, pour des algorithmes spécifiques (arbres binaires de recherche, algorithmes distribués), comme modèle abstrait pour des données semi-structurées utilisées pour l'échange d'information dans le Web, pour une présentation .....

Accès au texte intégral et bibtex

Titre

The Emptiness Problem for Tree Automata with Global Constraints

Auteurs

Barguñó Luis; Creus Carlos; Godoy Guillem; Jacquemard Florent; Vacher Camille

Détail

Jouannaud, Jean-Pierre. 25th Annual IEEE Symposium on Logic in Computer Science (LICS), July 2010, Edinburgh, Scotland, United Kingdom. IEEE Computer Society Press, pp. 263-272

DOI

DOI : 10.1109/LICS.2010.28

Accès au texte intégral et bibtex

Titre

Rewrite-Based Verification of XML Updates

Auteurs

Florent Jacquemard; Michael Rusinowitch

Détail

Kutsia, Temur and Schreiner, Wolfgang and Fernández, Maribel. 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), July 2010, Hagenberg, Austria. ACM

DOI

DOI : 10.1145/1836089.1836105

Accès au texte intégral et bibtex

long version:

Titre

XML Access Control: from XACML to Annotated Schemas

Auteurs

Ryma Abassi; Florent Jacquemard; Michael Rusinowitch; El Fatmi Sihem Guemara

Détail

Second International Conference on Communications and Networking (ComNet), November 2010, Tozeur, Tunisia. IEEE Computer Society Press, pp. 1-8

DOI

DOI : 10.1109/COMNET.2010.5699810

Accès au bibtex

Titre

Unique Normalization for Shallow TRS

Auteurs

Godoy Guillem; Jacquemard Florent

Détail

Treinen, Ralf. 20th International Conference on Rewriting Techniques and Applications (RTA), June 2009, Brazilia, Brazil. Springer, 5595, pp. 63-77, Lecture Notes in Computer Science

DOI

DOI : 10.1007/978-3-642-02348-4_5

Accès au texte intégral et bibtex

Titre

Rigid Tree Automata

Auteurs

Jacquemard Florent; Klay Francis; Vacher Camille

Détail

Adrian Horia Dediu and Armand Mihai Ionescu and Carlos Martín-Vide. Third International Conference on Language and Automata Theory and Applications, April 2009, Tarragona, Spain. Springer, 5457, pp. 446-457, Lecture Notes in Computer Science

DOI

DOI : 10.1007/978-3-642-00982-2_38

Accès au texte intégral et bibtex

Titre

Automatic Verification of Conformance of Firewall Configurations to Security Policies

Auteurs

Ben Youssef Nihel; Bouhoula Adel; Jacquemard Florent

Détail

IEEE Symposium on Computers and Communications (ISCC), July 2009, Sousse, Tunisia. IEEE Computer Society Press, pp. 526-531

DOI

DOI : 10.1109/ISCC.2009.5202309

Accès au texte intégral et bibtex

Titre

Visibly Tree Automata with Memory and Constraints

Auteurs

Comon-Lundh Hubert; Jacquemard Florent; Perrin Nicolas

Détail

Logical Methods in Computer Science (LMCS), Thompson ISI and SCOPUS and Mathematical Reviews and Zentralblatt, 2008, 4 (2)

DOI

DOI : 10.2168/LMCS-4(2:8)2008

Accès au texte intégral et bibtex

Titre

Tree automata with equality constraints modulo equational theories

Auteurs

Florent Jacquemard; Michael Rusinowitch; Laurent Vigneron

Détail

Journal of Logic and Algebraic Programming, Elsevier, 2008, 75 (2), pp. 182-208

DOI

DOI : 10.1016/j.jlap.2007.10.006

Accès au texte intégral et bibtex

Titre

Closure of Hedge-Automata Languages by Hedge Rewriting

Auteurs

Jacquemard Florent; Rusinowitch Michael

Détail

A. Voronkov. 19th International Conference on Rewriting Techniques and Applications - RTA 2008, 2008, Hagenberg, Austria. Springer Berlin / Heidelberg, Rewriting Techniques and Applications, 5117, pp. 157-171, Lecture Notes in Computer Science

DOI

DOI : 10.1007/978-3-540-70590-1_11

Accès au texte intégral et bibtex

Titre

Closure of Tree Automata Languages under Innermost Rewriting

Auteurs

Gascon Adria; Godoy Guillem; Jacquemard Florent

Détail

Middeldorp, Aart. 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS), July 2008, Hagenberg, Austria. Elsevier, Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2008), 237, pp. 23-38, Electronic Notes in Theoretical Computer Science

DOI

DOI : 10.1016/j.entcs.2009.03.033

Accès au texte intégral et bibtex

Titre

Automated Induction with Constrained Tree Automata

Auteurs

Bouhoula Adel; Jacquemard Florent

Détail

Alessandro Armando and Peter Baumgartner and Gilles Dowek. 4th International Joint Conference on Automated Reasoning (IJCAR), August 2008, Sydney, Australia. Springer, 5195, pp. 539-554, Lecture Notes in Computer Science

DOI

DOI : 10.1007/978-3-540-71070-7_44

Accès au texte intégral et bibtex

Titre

Tree Automata with Memory, Visibility and Structural Constraints

Auteurs

Hubert Comon-Lundh; Florent Jacquemard; Nicolas Perrin

Détail

Helmut Seidl. 10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), Mar 2007, Braga, Portugal. Springer, 10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), 4423, pp. 168-182, Lecture Notes in Computer Science

DOI

DOI : 10.1007/978-3-540-71389-0_13

Accès au texte intégral et bibtex

Titre

Verifying Regular Trace Properties of Security Protocols with Explicit Destructors and Implicit Induction

Auteurs

Adel Bouhoula; Florent Jacquemard

Détail

Degano, Pierpaolo and K{ü}sters, Ralf and Vigan{\ó}, Luca and Zdancewic, Steve. Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), Jul 2007, , Poland. Proceedings of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), pp. 27-44

Accès au texte intégral et bibtex

Titre

Tree Automata Techniques and Applications

Auteurs

Comon-Lundh Hubert; Dauchet Max; Gilleron, Rémi; Löding Cristof; Jacquemard Florent; Lugiez Denis; Tison Sophie; Tommasi Marc

Détail

Online book available on: http://tata.gforge.inria.fr

Accès au texte intégral et bibtex