Projects

Project LCHIP aims at largely facilitating the development of sure applications to high level of criticality while providing: - an environment of complete development allowing to generate and prove mathematically and automatically software with limited algorithmic, - a secure platform and at low cost for the execution of these application, in order to guarantee a maximum level of safety. Transparent integration with languages trade (DSL) and third line productions of code authorize a deployment without pain in existing development processes and support the exploitation of technology apart from the consortium.

The Mopsa project aims at creating methods and tools to make computer software more reliable. Programming errors are pervasive with results ranging from user frustration to huge economical or human losses. Traditional test-based methods are insufficient to eliminate all errors. The project will develop static analyses able to detect at compile-time whole classes of program defects, leveraging the theory of abstract interpretation to design analyses that are approximate (to scale up to large programs) and sound (no defect is missed). Static analysis has enjoyed recent successes: Astrée, an industrial analyzer, was able to prove the absence of run-time error in Airbus software. But such results are limited to the specific, well-controlled context of critical embedded systems. We wish to bring static analysis to the next level: target larger, more complex and heterogeneous software, and make it usable by engineers to improve general-purpose software. We focus on analyzing open-source software which are readily available, complex, widespread, and important from an economical standpoint (they are used in many infrastructures and companies) but also societal and educational ones (promoting the development of verified software for and by citizens). A major target we consider is the set of technologies at the core of Internet on which static analysis could be applied to ensure a safer Internet. The scientific challenges we must overcome include designing scalable analyses producing relevant information, supporting novel popular languages (such as Python), analyzing properties more adapted to the continuous development of software common in open-source. At the core of the project is the construction of an open-source static analysis platform. It will serve not only to implement and evaluate the results of the project, but also create a momentum encouraging the research in static analysis and hasten its adoption in open-source development communities.

Verifying correctness and robustness of programs and systems is a major challenge in a society which relies more and more on safety-critical systems controlled by embedded software. This issue is even more critical when the computations involve floating-point number arithmetic, an arithmetic known for its quite unusual behaviors, and which is increasingly used in embedded software. Note for example the "catastrophic cancellation" phenomenon where most of the significant digits of a result are cancelled or, numerical sequences whose limit is very different over the real numbers and over the floating-point numbers. A more important problem arises when we want to analyse the relationship between floating-point computations and an "idealized" computation that would be carried out with real numbers, the reference in the design of the program. The point is that for some input values, the control flow over the real numbers can go through one conditional branch while it goes through another one over the floating-point numbers. Certifying that a program, despite some control flow divergences, computes what it is actually expected to compute with a minimum error is the subject of the robustness or continuity analysis. Providing a set of techniques and tools for verifying the accuracy, correctness and robustness for critical embedded software is a major challenge. The aim of this project is to address this challenge by exploring new methods based on a tight collaboration between abstract interpretation (IA) and constraint programming (CP). In other words, the goal is to push the limits of these two techniques for improving accuracy analysis, to enable a more complete verification of programs using floating point computations, and thus, to make critical decisions more robust. The cornerstone of this project is the combination of the two approaches to increase the accuracy of the proof of robustness by using PPC techniques, and, where appropriate, to generate non-robust test cases. The goal is to benefit from the strengths of both techniques: PPC provides powerful but computationally expensive algorithms to reduce domains with an arbitrary given precision whereas AI does not provide fine control over domain precision, but has developed many abstract domains that quickly capture program invariants of various forms. Incorporating some PPC mechanisms (search tree, heuristics) in abstract domains would enable, in the presence of false alarms, to refine the abstract domain by using a better accuracy. The first problem to solve is to set the theoretical foundations of an analyser based on two substantially different paradigms. Once the interactions between PPC and IA are well formalized, the next issue is to handle constraints of general forms and potentially non-linear abstract domains. Last but not least, an important issue concerns the robustness analysis of more general systems than programs, like hybrid systems which are modeling control command programs. Research results will be evaluated on realistic benchmarks coming from industrial companies, in order to determine their benefits and relevance. For the explored approaches, using realistic examples is a key point since the proposed techniques often only behave in an acceptable manner on a given sub classes of problems (if we consider the worst-case computational complexity all these problems are intractable). That's why many solutions are closely connected to the target problems.

The evolution of scientific knowledge is directly related to the history of humanity. Document archives and bibliographic sources like the “Web Of Science” or PubMed contain a valuable source for the analysis and reconstruction of this evolution. The proposed project takes as starting point the contributions of D. Chavalarias and J.P. Cointet about the analysis of the dynamicity of evolutive corpora and the automatic construction of “phylomemetic” topic lattices (as an analogy with genealogic trees of natural species). Currently existing tools are limited to the processing of medium sized collections and a non interactive usage. The expected project outcome is situated at the crossroad between Computer science and Social sciences. Our goal is to develop new highly performant tools for building phylomemetic maps of science by exploiting recent technologies for parallelizing tasks and algorithms on complex and voluminous data. These tools are conceived and validated in collaboration with experts in philosophy and history of science over large scientific archives. Keywords : quantitative epistemology, evolution of science, topic detection, temporal alignment, big data processing, data science, big data

Experimaestro is an experiment manager based on a server that contains a job scheduler (job dependencies, locking mechanisms) and a framework to describe the experiments with JavaScript or in Java.

A common way to achieve scalability for processing SPARQL queries over large RDF data sets is to choose map-reduce frameworks like Hadoop or Spark. Processing complex SPARQL queries generating large join plans over distributed data partitions is a major challenge in these shared nothing architectures. In this article we are particularly interested in two representative distributed join algorithms, partitioned join and broadcast join, which are deployed in map-reduce frameworks for the evaluation of complex distributed graph pattern join plans. We compare five SPARQL graph pattern evaluation implementations on top of Apache Spark to illustrate the importance of cautiously choosing the physical data storage layer and of the possibility to use both join algorithms to take account of the existing predefined data partitionings. Our experimentations with different SPARQL benchmarks over real-world and synthetic workloads emphasize that hybrid join plans introduce more flexibility and often can achieve better performance than join plans using a single kind of join implementation.

Block-o-Matic is a web page segmentation algorithm based on an hybrid approach for scanned document segmentation and visual-based content segmentation. A web page is associated with three structures: the DOM tree, the content structure and the logical structure. The DOM tree represents the HTML elements of a page, the geometric structure organizes the content based on a category and its geometry and finally the logical structure is the result of mapping content structure on the basis of the human-perceptible meaning that conforms the blocks. The segmentation process is divided in three phases: analysis, understanding and reconstruction of a web page. An evaluation method is proposed in order to perform the evaluation of web page segmentations based on a ground truth of 400 pages classified into 16 categories. A set of metrics are presented based on geometric properties of blocks. Satisfactory results are reached when comparing to other algorithms following the same approach.

Coriolis is an experimental integrated platform for the research, development and evaluation of new back-end VLSI design flows. Interconnect scaling to nanometer processes presents many difficult challenges to CAD flows. Currently academic research on back-end tend to address only specific algorithmic issues separately, although one key issue to address is the cooperation of multiple algorithmic tools. CORIOLIS, our platform, is based on an integrated C++ database around which all tools consistently interact and collaborate. This platform currently includes a timing-driven global place and route flow.

Our purpose is to provide a language for designing generators of analog functions, that can be easily ported to new set of specfications and new technologogy processes. We are currently developing such a language that is called CAIRO+ The CAIRO+ language supports the four steps of a design flow based on net-list and layout templates. This language is aimed to help the designer to capture his knowledge, thus creating a library of layout-aware analog functions. It is based on C++ language. The design flow relevant to CAIRO+ is the following : ->net-list and layout template capture, ->design space exploration (managing electrical constraints) ->shape function computation (managing geometrical constraints) ->layout generation (place and route) CAIRO+ allows creating complex hierarchical analog function generators by using existing generators of simpler functions. It is an answer to the problem of Analog and Mixed IPs. As a demonstration of the CAIRO+'s capabilities, we are developping Analog to Digital converters, specially Sigma Delta.

Lemon is a GUI toolkit written in C++ for manipulating graphical models. It relies on aGrUM both for graph theoretic algorithms and for computations within the graphical models (e.g., inference, learning).

aGrUM is a C++ library designed for easily manipulating graphical models. Its range of applications is quite large as it is designed, e.g., for performing learning tasks (for instance, learning Bayes nets from data), planning tasks (FMDPs) and inference (Bayes nets, GAI-nets, influence diagrams).

MAGAM is a Multi-Aspect (didactic, pedagogic, affective and motivational, gaming, etc.) Generic Adaptation Model based on matrix calculation that aims to adapt learning activities.

NeoPraEval is an ANR-funded research project which aims at providing tools for teachers to deal with heterogeneity in learning through automatic diagnostic and evaluation systems that they can use in their classes, as well as appropriated resources to answer the needs identified in students.

RecoMOOC aims at reducing attrition and improving the learning experience for MOOC learners through interaction with other students they can talk to and work with, identified automatically through a peer recommender system analyzing each learner's individual factors and progression.

PNML Framework is a prototype implementation of ISO/IEC-15909 part 2, International Standard on Petri Net Markup Language. The primary purpose of PNML is to enable interoperability among Petri net tools. PNML framework has thus been designed to back the Standard. It will enable Petri nets tools developers to seamlessly integrate PNML support into their tools. It provides an extensive and comprehensible API to create, save, load and browse PNML models.

PolyORB is a join project between LIP6 and Telecom Paris

is a Petri Net based CASE environment. It offers a set of services to perform specification, validation, formal verification, model checking, compute structural properties (invariants, traps, syphons etc.) simulate and generate code. These services have been implemented either by members of our team or university partners (Technical university of Helsinki, University of Torino, Technical university of Munchen, Bell laboratories). The second geration of CPN-AMI, build on top of FrameKit, is available on the Internet since March 1997.

SPOT (Spot Produces Our Traces) est une bibliothèque de model-checking facilement extensible. À la différence des model-checkers existants, dont le mode opératoire est immuable, SPOT fournit des briques que l'utilisateur peut combiner entre elles pour réaliser un model-checker répondant à ses propres besoins. Une telle modularité permet d'expérimenter facilement différentes combinaisons, et facilite le développement de nouveaux algorithmes. D'autre part, cette bibliothèque est centrée autour d'un type d'automates particulier permettant d'exprimer les propriétés à vérifier de façon plus compacte, qui n'a jamais été utilisé dans un outil jusqu'à présent.

Remote interoperability testing services for IoT devices

CADNA is a library which allows to perform scientific computations with the estimation and the control of the round-off error propagation.

Disaster-based disruptions seriously degrading the performance of any communication network (following from natural disasters, technology-related disasters, or malicious attacks) are now gaining importance due to observed increase of their intensity and scale. The problem is of the utmost importance due to lack of appropriate mechanisms deployed in practice in Europe. Each time, unavailability of communication networks services, considered as an important part of critical infrastructure, in the presence of disasters implies evident societal problems for people desperately seeking for information, or trying to communicate with each other. The Action will fill this gap by offering the respective solutions to provide resilient communications in the presence of disaster-based disruptions of all types for existing communication networks (e.g., IPv4-based, current Internet), as well as emerging architectures of the global communications infrastructure (i.e., the Future Internet). Geographical diversity characteristics of disaster-based disruptions across Europe requires creation of an international and geographically diverse group of researchers to provide the proper solutions. Therefore, COST Action is viewed as the best way to address this issue. This output-oriented Action will be driven by researchers from academia and industry in strong cooperation with governmental bodies. The aim is to introduce the set of techniques of resilient communications, as well as recommendations on how to deploy/update topologies of communication networks to make them resistant to disruptions that can be applied in practice by network equipment operators and national/international network providers at the European level.

WIth about 50 European research institutions.