Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > LIFO Research Report for Year 2017

 Site en Français



Contact

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



Go to Research Reports of Year : 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017

LIFO Research Report for Year 2017


RR-2017-01 Transforming Prefix-Constrained or Controlled Rewrite Systems
Nirina Andrianarivelo, Vivien Pelletier, Pierre Réty
Date : 2017-02-03
Abstract Download

RR-2017-02 Handling limits of high degree vertices in graph processing using MapReduce and Pregel
M. Al Hajj Hassan and Mostafa Bamha
Date : 2017-02-27
Abstract Download

RR-2017-03 Concurrent Program Verification by Code Transformation: Correctness
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Date : 2017-03-08
Abstract Download


Abstracts of Research Reports


RR-2017-01 Transforming Prefix-Constrained or Controlled Rewrite Systems
Nirina Andrianarivelo, Vivien Pelletier, Pierre Réty
Abstract : We present two techniques for transforming any prefix-cons\-trained and any controlled term rewrite system into an ordinary rewrite system. We prove that both transformations preserve the rewrite computations, and preserve termination. In this way, prefix-constrained rewriting and controlled rewriting can be run, and termination can be checked, using the usual tools for ordinary rewriting.
Keywords : controlled rewriting, prefix constrained rewriting, tree automaton.

RR-2017-02 Handling limits of high degree vertices in graph processing using MapReduce and Pregel
M. Al Hajj Hassan and Mostafa Bamha
Abstract : Even if Pregel scales better than MapReduce in graph processing by reducing iteration's disk I/O, while offering an easy programming model using "think like vertex" approach, large scale graph processing is still challenging in the presence of high degree vertices: Communication and load imbalance among processing nodes can have disastrous effects on performance. In this paper, we introduce a scalable MapReduce graph partitioning approach for high degree vertices using a master/slave partitioning allowing to balance communication and computation among processing nodes during all the stages of graph processing. Cost analysis and performance tests of this partitioning are given to show the effectiveness and the scalability of this approach in large scale systems.
Keywords : Graph processing, High degree vertices, Data skew, MapReduce programming model, Pregel, Distributed file systems.

RR-2017-03 Concurrent Program Verification by Code Transformation: Correctness
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Abstract : Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed conc2seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program trans- formation principle behind conc2seq, and present an effort towards the full mecha- nization of both the formalization and proofs with the proof assistant Coq.
Keywords :