- Renseignements pratiques
- Enseignement

**LIFO** - Bâtiment IIIA

Rue Léonard de Vinci

B.P. 6759

F-45067 ORLEANS Cedex 2

**Email:**
contact.lifo

**Tel:** +33 (0)2 38 41 70 11

**Fax:** +33 (0)2 38 41 71 37

Accéder aux Rapports de l'année : 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017

# Les rapports de recherche du LIFO en 2010

## Résumés des rapports de recherche

**RR-2010-01** Systematic Development of Functional Bulk Synchronous Parallel Programs

*Julien Tesson, Zhenjiang Hu, Kiminori Matsuzaki, Frédéric Loulergue, Louis Gesbert*

**Résumé : **With the current generalization of parallel architectures arises the concern of applying formal methods to parallelism, which allows specifications of parallel programs to be precisely stated and the correctness of an implementation to be verified. However, the complexity of parallel, compared to sequential, programs makes them more error-prone and difficult to verify. This calls for a strongly
structured form of parallelism, which should not only ease programming by providing abstractions that conceal much of the complexity of parallel computation, but also provide a systematic way of developing practical programs from specification.
Bulk Synchronous Parallelism (BSP) is a model of computation which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism. We propose a framework for refining a sequential specification toward a functional BSP program, the whole process being done with the help of a proof assistant. The main technical contributions of this paper are as follows: We define BH, a new homomorphic skeleton, which captures the essence of BSP computation in an algorithmic level, and also serves as a bridge in mapping from high level specification to low level BSP parallel programs~; We develop a set of useful theories in Coq for systematic and formal derivation of programs in BH from specification, and we provide a certified parallel implementation of BH in the parallel functional language Bulk Synchronous Parallel ML so that a certified BSP parallel program can be automatically extracted from the proof; We demonstrate with an example that our new framework can be very useful in practice to develop certified BSP parallel programs.

**Mot(s) Clé(s) : **

**RR-2010-02** Functional Term Rewriting Systems

*Yohan Boichut, Jean-Michel Couvreur, Duy-Tung Nguyen*

**Résumé : **This reseach report proposes the theoretical foundations of a new formal tool for symbolic verification of finite systems. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs). In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called Functional Term Rewriting Systems (FTRSs). First, we show that FTRSs are as expressive as TRSs. Then, we focus on a subclass of FTRSs, so called Elementary Functional Term Rewriting Systems (EFTRSs), and we show that EFTRSs preserve the FTRSs expressiveness. The main advantage of EFTRSs is that they are well adapted for acceleration techniques usually used in saturation algorithms on BDD-like data structures. Our experiments show that for well-known protocols (e.g. Tree Arbiter, Percolate, Round Robin Mutex protocols,...) our tool is not only better than other rewriting tools such as Timbuk or Maude, but also competitive with other model-checkers such as SPIN, NuSMV or SMART. Moreover, it can also be applied to model-checking invariant properties which are a particular subclass of linear temporal logic formula (LTL).

**Mot(s) Clé(s) : **

**RR-2010-03** Discriminative Markov Logic Network Structure Learning based on Propositionalization and chi2-test

*Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN*

**Résumé : **In this paper we present a bottom-up discriminative algorithm to automatically learn Markov Logic Network structures. Our approach relies on a new propositionalization method that transforms the learning dataset into an approximative representation in the form of a boolean table. Using this table, the algorithm constructs a set of candidate clauses according to a chi2 independence test. To compute and choose clauses, we successively use two different optimization criteria, namely log-likelihood (LL) and conditional log-likelihood (CLL), in order to combine the efficiency of LL optimization algorithms together with the accuracy of CLL ones. First experiments show that our approach outperforms existing discriminative MLN structure learning algorithms.

**Mot(s) Clé(s) : **Markov Logic Network, Structure Learning, Relational Learning, Propositionalization, Inductive Logic Programming

**RR-2010-04** Interactive and progressive constraint definition for dimensionality reduction and visualization

*Lionel Martin, Matthieu Exbrayat, Guillaume Cleuziou, Frédéric Moal *

**Résumé : **In this paper we focus on semi-supervised dimensionality reduction. Projecting and visualizing objects in a low dimension space is a current data analysis task. From another point of view, several works have been conducted recently, that constrain the projection space in order to optimize a given criteria (e.g. classification according to nearest neighbors). Nevertheless, none of those offers a satisfying interaction level. We thus propose an approach that offers to the user the ability to interactively add knowledge in the form of (di)similarity constraints among objects, when those appear either to close or to far in the current observation space. Such constraints can be added iteratively, the projection being modified after each new constraint. We propose several kinds of constraints and present a resolution method that derives from PCA. Experiments have been performed with both synthetic and usual datasets. They show that a satisfying representation (w.r.t a given quality criterion) can be obtained with a small set of constraints.

**Mot(s) Clé(s) : **semi supervised learning, dimensionality reduction.

**RR-2010-05** Heuristic Method for Discriminative Structure Learning of Markov Logic Networks

*Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN*

**Résumé : **Markov Logic Networks (MLNs) combine Markov
Networks and first-order logic by attaching weights to firstorder
formulas and viewing them as templates for features
of Markov Networks. Learning a MLN can be decomposed
into structure learning and weights learning. In this paper,
we present a heuristic-based algorithm to learn discriminative
MLN structures automatically, directly from a training dataset.
The algorithm heuristically transforms the relational dataset
into boolean tables from which to build candidate clauses for
learning the final MLN. Comparisons to the state-of-the-art
structure learning algorithms for MLNs in the three real-world
domains show that the proposed algorithm outperforms them
in terms of the conditional log likelihood (CLL), and the area
under the precision-recall curve (AUC).

**Mot(s) Clé(s) : **Markov Logic Network, Structure Learning, Discriminative learning, Relational Learning.

**RR-2010-06** Security and Virtualization: a Survey

*Patrice Clemente, Jonathan Rouzaud-Cornabas*

**Résumé : **In this report, we investigate the security aspects and challenges about computer
virtualization. In a few words, virtualization is what allows the execution of multiple operating systems on a single machine at the same time. A virtualization
component can be viewed as a layer or a container making some kind of emulation, allowing to execute programs or operating systems on the virtualized layer,
for example executing Microsoft Windows and Linux on one single machine at
the same time. On one hand, as virtualization can provide a kind of isolation between users/applications/operating systems, it can address some security containment problems. But on the other hand, there exist today many security flaws and
attacks focused on such systems, as the virtualization layer controls and monitors
all virtualized applications/operating systems.
The outline of this report is the following. We first review precisely all the
various forms the virtualization layer and related components can take. And what
technical aspects it involves. Then we survey more precisely all the vulnerabilities
and exploits that currently exist or may appear in the near future. And then we
study what are the proposed security protection by actual virtualization technologies. We conclude the report with what is remaining to be done and what are the
forthcoming security challenges.

**Mot(s) Clé(s) : **

**RR-2010-08** Fractal Parallelism: Solving SAT in bounded space and time.

*Denys Duchier, Jérôme Durand-Lose, Maxime Senot.*

**Résumé : **Abstract geometrical computation can solve NP-complete problems efficiently: any boolean constraint satisfaction problem, instance of SAT, can be solved in bounded space and time with simple geometrical constructions involving only drawing parallel lines on a Euclidean space-time plane. Complexity as the maximal length of a sequence of consecutive segments is quadratic. The geometrical algorithm achieves massive parallelism: an exponential number of cases are explored simultaneously. The construction relies on a fractal pattern and requires the same amount of space and time independently of the SAT formula.

**Mot(s) Clé(s) : **Abstract geometrical computation; Signal machine; Fractal; SAT; Massive parallelism; Model of computation.

**RR-2010-09** ON REMOVABLE EDGES IN 3−CONNECTED CUBIC GRAPHS

*Jean-Luc FOUQUET, Henri THUILLIER*

**Résumé : **A removable edge in a 3−connected cubic graph G is an edge e = uv such that the cubic graph obtained from G \ {u, v} by adding an edge between the two neighbours of u distinct from v and an edge between the two neighbours of v disctinct from u is still 3−connected. Li and Wu [3] showed that a spanning tree in a 3−connected cubic graph avoids at least two removable edges, and Kang, Li and Wu [4] showed that a spanning tree contains at least two removable edges. We show here how to obtain these results easily from the structure of the sets of non removable edges and we give a characterization of the extremal graphs for these two results.

**Mot(s) Clé(s) : **Cubic graph, Removable edge, spanning trees

**RR-2010-10** Tools for parsimonious edge-colouring of graphs with maximum degree three

*J.L. Fouquet and J.M. Vanherpe*

**Résumé : **In a graph G of maximum degree Delta let gamma denote the largest fraction of edges that can be Delta edge-coloured. Albertson and Haas showed that gamma >=13/15G is cubic . The notion of delta-minimum edge colouring was introduced by the first author in order to extend the so called parcimonious edge-colouring to graphs with maximum degree 3. We propose here an english translation of some structural properties already present in previous papers (in French) for delta-$minimum edge colourings of graphs with maximum degree 3.

**Mot(s) Clé(s) : **Cubic graph; Edge-colouring

**RR-2010-11** A new bound for parsimonious edge-colouring of graphs with maximum degree three

*J.L. Fouquet and J.M. Vanherpe*

**Résumé : **In a graph G of maximum degree 3, let gamma(G) denote the largest fraction of edges that can be 3 edge-coloured. Rizzi showed that gamma(G) >=1-2/(3godd(G)) where godd(G) is the odd girth of G, when G is triangle-free. In a previous paper we extended that result to graph with maximum degree 3. We show here that gamma(G) >=1-2/(3good(G)+2), which leads to gamma(G) >= 15/17 when considering graphs with odd girth at least 5, distinct from the Petersen graph.

**Mot(s) Clé(s) : **

**RR-2010-12** Syntaxe et sémantique de Revised Bulk Synchronous Parallel ML

*Wadoud Bousdira, Frédéric Loulergue, Louis Gesbert*

**Résumé : **Bulk Synchronous Parallel ML (BSML) est une extension du langage fonctionnel Objective Caml, fondé sur un modèle structuré de parallélisme, le modèle BSP. Ce modèle assure au programmeur BSML la sûreté d'exécution tout en lui laissant le strict contrôle des processeurs. Le modèle de prévision de performances de BSML est simple et réaliste. Le parallélisme est exprimé en utilisant un ensemble de primitives fonctionnelles pures sur une structure de données parallèle appelée vecteur parallèle. Cependant, les programmes sont souvent difficiles à écrire et leur mise au point peut être fastidieuse. Nous proposons dans cet article une nouvelle syntaxe et une sémantique associée dans le but d'écrire des programmes plus courts et plus lisibles. Nous formalisons la syntaxe et la sémantique classiques ainsi que les nouvelles syntaxe et sémantique, puis nous les modélisons en Coq. Leur confluence est établie.

**Mot(s) Clé(s) : **

**RR-2010-13** Comparaison des langages d'arbres dans le cadre de la substitution de services web

*Joshua Amavi*

**Résumé : **Dans ce rapport, nous proposons un algorithme qui étend l'inclusion relâchée sur les arbres à l'inclusion relâchée sur les langages d'arbres.
Notre algorithme est utile dans le contexte de la substitution de service web, et plus précisément pour la comparaison de schéma XML.
L'algorithme repose sur les langages synchronisés de couples d'arbres. L'algorithme a été prouvé correct et implémenté en Prolog.

**Mot(s) Clé(s) : **Langage d'arbres, inclusion relâchée de schéma XML, service web, langage synchronisé de couples d'arbres, expression régulière

**RR-2010-01**
Systematic Development of Functional Bulk Synchronous Parallel Programs
*Julien Tesson, Zhenjiang Hu, Kiminori Matsuzaki, Frédéric Loulergue, Louis Gesbert*

Date : 2010-03-22

Résumé Télécharger

**RR-2010-02**
Functional Term Rewriting Systems
*Yohan Boichut, Jean-Michel Couvreur, Duy-Tung Nguyen*

Date : 2010-05-18

Résumé Télécharger

**RR-2010-03**
Discriminative Markov Logic Network Structure Learning based on Propositionalization and chi2-test
*Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN*

Date : 2010-05-21

Résumé Télécharger

**RR-2010-04**
Interactive and progressive constraint definition for dimensionality reduction and visualization
*Lionel Martin, Matthieu Exbrayat, Guillaume Cleuziou, Frédéric Moal *

Date : 2010-05-21

Résumé Télécharger

**RR-2010-05**
Heuristic Method for Discriminative Structure Learning of Markov Logic Networks
*Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN*

Date : 2010-09-02

Résumé Télécharger

**RR-2010-06**
Security and Virtualization: a Survey
*Patrice Clemente, Jonathan Rouzaud-Cornabas*

Date : 2010-12-31

Résumé Télécharger

**RR-2010-08**
Fractal Parallelism: Solving SAT in bounded space and time.
*Denys Duchier, Jérôme Durand-Lose, Maxime Senot.*

Date : 2010-09-16

Résumé Télécharger

**RR-2010-09**
ON REMOVABLE EDGES IN 3−CONNECTED CUBIC GRAPHS
*Jean-Luc FOUQUET, Henri THUILLIER*

Date : 2010-09-09

Résumé Télécharger

**RR-2010-10**
Tools for parsimonious edge-colouring of graphs with maximum degree three
*J.L. Fouquet and J.M. Vanherpe*

Date : 2010-10-12

Résumé Télécharger

**RR-2010-11**
A new bound for parsimonious edge-colouring of graphs with maximum degree three
*J.L. Fouquet and J.M. Vanherpe*

Date : 2010-10-12

Résumé Télécharger

**RR-2010-12**
Syntaxe et sémantique de Revised Bulk Synchronous Parallel ML
*Wadoud Bousdira, Frédéric Loulergue, Louis Gesbert*

Date : 2010-11-02

Résumé Télécharger

**RR-2010-13**
Comparaison des langages d'arbres dans le cadre de la substitution de services web
*Joshua Amavi*

Date : 2010-12-17

Résumé Télécharger

Université d'Orléans | INSA Centre Val de Loire