Software LIP6

SAFE : Stochastic Arithmetic with Flexible Exponent

SAFE permet d'estimer les erreurs d'arrondi et de détecter les instabilités numériques dans les programmes où les nombres flottants ont une mantisse et un exposant de taille arbitraire.

Project Leader : Fabienne JEZEQUEL

09/2024

https://www-pequan.lip6.fr/~jezequel/SAFE

QOSST : Quantum Open Software for Secure Transmissions

An open source suite to perform Continuous Variable Quantum Key Distribution.

Project Leader : Eleni Diamanti

04/2024

https://github.com/qosst/

OMicroB : OCaml on Microcontroller Boards

OMicroB est une implémentation spécialisée de la machine virtuelle OCaml conçue pour fonctionner sur des microcontrôleurs aux ressources limitées. Cette implémentation peut en effet exécuter des programmes OCaml non triviaux sur de petits microcontrôleurs, et fournit au développeur de logiciels embarqués tous les paradigmes de programmation de haut niveau du langage OCaml (fonctionnel, impératif, modulaire, orienté objet) ainsi qu'une sécurité accrue grâce au typage statique et à la gestion automatique de la mémoire. La chaîne de compilation d’OMicroB prend un exécutable en byte-code directement produit par le compilateur OCaml et après plusieurs passes d’analyse (détection de code mort, évaluation partielle, …) produit un code C standard embarquant la VM, sa bibliothèque d’exécution et le byte-code transformé. Ce code C produit, hautement portable, cible différentes architectures de microcontrôleurs et peut être compilé et exécuté sur un PC standard à des fins de simulation et de débogage.

Project Leader : Emmanuel CHAILLOUX

04/2023

https://github.com/stevenvar/OMicroB

MQ Soft : A fast multivariate cryptography library

MQsoft is an efficient library in C for post-quantum multivariate-based cryptography. It includes HFE-based schemes such GeMSS, Gui and DualModeMS. Our library is modular and permits to perform fundamental arithmetic operations over finite fields: efficient constant-time arithmetic in GF(2^n), finding the roots of a univariate polynomial in GF(2^n)[X], evaluate efficiently multivariate quadratic systems in GF(2) (in constant-time and in variable-time), etc ...

Project Leader : Ludovic Perret

01/2023

https://www-polsys.lip6.fr/Links/NIST/MQsoft.html

PML : Polynomial Matrix Library

This library provides additions to NTL: efficient implementations for operations on univariate polynomial matrices and structured scalar matrices, and some uses of these for related algebraic computations. Work in progress includes adding functionalities (algebraic relations, normal form computation) and providing similar additions based on Flint.

Project Leader : Vincent Neiger

01/2023

https://github.com/vneiger/pml

FuzzIC : Fuzzy Interpretability Checker

FuzzIC est une bibliothèque Python pour évaluer l'interprétabilité d'une base de règles floues. Il s'agit d'un outil en ligne de commande qui analyse automatiquement une base et qui génère un tableau de bord HTML interactif.

Dans FuzzIC, 20 critères d'interprétabilité différents sont implémentés et leur agrégation permet d'obtenir un score global d'interprétabilité d'une base de règles floues. Dans cette librairie, plusieurs outils d'évaluation configurables, flexibles et personnalisables sont aussi fournis.

Ce travail a été réalisé dans le cadre du projet ANR-22-ASTR-0032 IFP-in-RL, financé par l'ANR, dans un partenariat entre Sorbonne Université/LIP6 et Thales.

Project Leader : Christophe MARSALA

01/2023

https://gitlab.lip6.fr/lfi/fuzzic

HPDDM : high-performance unified framework for domain decomposition methods

HPDDM est une collection de préconditionneurs basés sur le paradigme de la décomposition de domaine, avec ou sans recouvrement. Ils peuvent être utilisés pour résoudre de grands systèmes linéaires, comme on en rencontre généralement lors de la discrétisation d'équations aux dérivées partielles. Ces préconditionneurs peuvent être utilisés avec diverses méthodes Krylov. La bibliothèque est utilisable dans les codes C, C++, Python ou Fortran.

Project Leader : Pierre JOLIVET

12/2022

https://github.com/hpddm/hpddm

msolve : Multivariate polynomial systems solving

msolve est une bibliothèque écrite en C pour la résolution de systèmes polynomiaux multivariés. Elle s'appuie sur des méthodes algébriques, notamment le calcul de bases de Gröbner, et permet de résoudre de manière exacte des systèmes polynomiaux à coefficients à coefficients rationnels (isolation des racines réelles) ou dans un corps premier (de cardinalité inférieure à 2^31).

msolve inclut des implantations haute-performances des algorithmes réputés les plus efficaces. La librairie peut être utilisée depuis de nombreux systèmes calcul formel et est intégrée dans les systèmes OSCAR et SageMath.

msolve est développée en collaboration avec Christian Eder (TU Kaiserslautern, Allemagne).

Project Leader : Mohab Safey El Din

10/2022

https://msolve.lip6.fr

IOHprofiler : Iterative Optimization Heuristics Profiler

IOHprofiler, a benchmarking platform for evaluating the performance of iterative optimization heuristics (IOHs), e.g., Evolutionary Algorithms and Swarm-based Algorithms. See https://iohprofiler.github.io/ Licence:BSD-3

Project Leader : Carola Doerr

06/2021

https://iohprofiler.github.io/

SPY : SPY

SPY est un jeu sérieux pour initier les joueurs aux bases de la programmation informatique. Nous travaillons à travers ce projet différentes problématiques : comprendre les phénomènes d’apprentissage de l’informatique ; aider les enseignants à s'approprier, concevoir et scénariser un jeu sérieux pour l'apprentissage de la programmation informatique ; travailler l'accessibilité de l'apprentissage de la programmation pour des élèves à besoin particuliers.

Project Leader : Mathieu Muratet

01/2021

https://spy.lip6.fr/

ScenoClasse : ScenoClasse

ScenoClasse est un outil de scénarisation issu de la recherche et destiné aux enseignants. Il leur permet de préparer leurs séances autour de l’informatique/ la pensée informatique. ScenoClasse permet aux enseignants de créer, éditer, documenter et agencer des activités d’enseignement de la pensée informatique en scénarios puis de publier et d’exporter ces scénarios sous différents formats de sortie (fiche de préparation papier ou sur tablette/téléphone, diaporama, etc.). Ils peuvent également copier et adapter des scénarios créés par d’autres. Chaque scénario rendu public sur la plateforme ScenoClasse peut être enrichi collectivement par des commentaires et des retours d’expériences. Ces fonctionnalités ont été pensées pour permettre à un scénario d’avoir un cycle de vie au-delà du contexte prévu par son auteur.

Project Leader : Amel Yessad

01/2021

https://scenoclasse.lip6.fr/

MUMPS : MUltifrontal Massively Parallel Sparse direct Solver

Logiciel de résolution de systèmes linéaires creux. La collaboration du LIP6 avec Mumps Tech SAS porte sur l'utilisation de représentations de rang faible en précision mixte, dans le contexte de la thèse CIFRE de M. Gerest financée par EDF.

Project Leader : Théo MARY

11/2020

http://mumps-solver.org/

AffApy : python library for multiprecision Affine Arithmetic

AffApy est une bibliothèque Python pour du calcul en arithmétique affine multiprécision

Project Leader : Thibault HILAIRE

01/2020

https://gitlab.lip6.fr/hilaire/affapy

CosyVerif : Software Environment for the Formal Specification and Verification of Dynamic Systems

CosyVerif est un environnement logiciel permettant la spécification formelle et la vérification de systèmes dynamiques.

Project Leader : Fabrice KORDON

06/2019

http://www.cosyverif.org

PaInLeSS : PArallel INstantiabLE Sat Solver

Cet outil écrit en C++ simplifie l'implémentation et l'évaluation de nouveaux solveurs pour des environnements multi-coeurs. Les composants peuvent être instanciés indépendamment pour produire un nouveau solveur SAT .

Project Leader : Souheib Baarir

06/2019

https://github.com/lip6/painless

BCMCyPhy : Component model for cyber-physical control systems

Ce projet de recherche et le logiciel associé visent à concevoir et implanter un modèle de programmation par composants pour les systèmes de contrôle cyber-physique. Il se greffe sur le projet BCM4Java dont il utilise les concepts de base et l'implantation des composants répartis en Java (10.000 lignes de code et de documentation à ce jour). Outre le fait d'intégrer des composants temps réel, ce projet étudie les architectures de contrôle (automatique) à base de composants, leur spécification utilisant les systèmes hybrides stochastiques et leur simulation utilisation des modèles de simulation suivant la norme DEVS. Une attention particulière est portée sur la composabilité parallèle entre les composants, leurs spécifications et leurs modèles de simulation individuels. Un sous-projet logiciel de BCMCyPhy propose une nouvelle implantation en Java de la norme DEVS pour la simulation modulaire des composants et de leurs assemblages (20.000 lignes de code et de documentation à ce jour)). Les simulateurs obtenus par composition entre simulateurs de chaque composant permettent ensuite de mettre au point, tester, vérifier et valider les applications. Ce logiciel a été utilisé par quelques dizaines d'étudiants et l'est toujours dans le cadre du cours de master 2 ALASCA depuis 2018.

Project Leader : Jacques MALENFANT

06/2019

Cosy : Symmetry controller

Cosy est une bibliothèque C++ efficace conçue pour casser dynamiquement les symétries dans la résolution de problèmes SAT. Elle s'appuie sur des solveurs SAT de l'état de l'art en intégrant un contrôleur de symétrie qui fonctionne de manière complémentaire avec l'algorithme CDCL (Conflict-Driven Clause Learning). Cosy peut être intégré à la plupart des solveurs CDCL, offrant flexibilité et performance améliorée, notamment dans les instances SAT hautement symétriques. Elle est disponible sous licence open-source GPL v3.

Project Leader : Souheib Baarir

04/2018

https://github.com/lip6/cosy

Dedale est le premier simulateur dédié à l’étude des problèmes de coordination, d’apprentissage et de prise de décision multi-agents sous hypothèses réalistes. Dedale offre des environnements discrets et continus, ouverts, dynamiques et partiellement observables dans un contexte totalement asynchrone. Il permet l’étude et l’évaluation de solutions multi-agents pour le problème de l’exploration, le problème de la patrouille, les problèmes des tournées de véhicules et de la collecte de ressources par des équipes de plusieurs dizaines d’agents hétérogènes. La variété des problèmes multi-agents modélisables associée à la possibilité de créer un réseau pair-a-pair d’instances Dedale permettent d’envisager que celui-ci devienne un environnement de référence, tant pour l’enseignement que la recherche.

Project Leader : Cédric Herpson

03/2018

https://dedale.gitlab.io/

MOPSA analyzer : MOPSA Static Analyzer

MOPSA est un logiciel de vérification de programmes multi-languages par analyse statique sûre basée sur la théorie de l'interprétation abstraite. Il infère automatiquement des invariants et détecte, à la compilation, les erreurs possibles à l'exécution. L'analyse calcule une interprétation des programmes dans une collection d'abstractions réutilisables et programmées en OCaml. Sa conception modulaire permet à MOPSA d'être extensible vis à vis des propriétés et des langages considérés. MOPSA supporte actuellement des sous-ensembles significatifs des langages C et Python 3. En C, MOPSA détecte les comportements indéfinis ainsi que l'utilisation invalide de la bibliothèque standard C (spécifiée dans un langage de modélisation dédié). En Python, MOPSA effectue une analyse de type, de valeur et des exceptions.

Project Leader : Antoine Miné

03/2018

https://gitlab.com/mopsa/mopsa-analyzer

TSAR : TSAR (Tera-Scale ARchitecture)

Project Leader : Alain Greiner

09/2017

https://www-soc.lip6.fr/trac/tsar

FiXiF : Reliable fixed-point implementation of linear signal processing (and control) algorithms

FiXiF est une suite d’outils utilisés pour implémenter des filters sur des systèmes embarqués (tels que DSP, micro-controlleurs, FPGA ou ASIC) avec l’impact de la précision finie (virgule fixe et flottante).

Project Leader : Thibault HILAIRE

08/2017

https://github.com/fixif/fixif

Wi-Fi Direct, also called Wi-Fi P2P, is a new communication mode in Wi-Fi networks, which allows nearby users to communicate directly without an infrastructure composing of access points. This project implements a simulation model for Wi-Fi Direct in the INET Framework of the OMNeT++ simulator. A new module, DuoHost, has been defined for the formation of a new Wi-Fi direct group or joining an existing one.

Project Leader : Thi Mai Trang NGUYEN

06/2017

https://www-phare.lip6.fr/~trnguyen/research/wifidirect

TTK : Topology ToolKit

Le Topology ToolKit (TTK) est une bibliothèque open source et une collection de logiciels pour l'analyse et la visualisation de données topologiques. TTK peut gérer des données scalaires définies soit sur des grilles régulières, soit sur des triangulations, en 2D, 3D ou plus. Il fournit une collection substantielle d'implémentations génériques, efficaces et robustes d'algorithmes clés dans l'analyse de données topologiques.

Project Leader : Julien Tierny

04/2017

https://topology-tool-kit.github.io/

E-LearningScape : E-LearningScape

E-LearningScape est un Serious Escape Game sur le thème de la pédagogie. Ce jeu, soutenu par Sorbonne Université, est une adaptation du jeu LearningScape conçu par SAPIENS et le CRI. Nous travaillons sur la conception d'un module de suivi des actions du joueur, afin de générer en temps réel des aides contextualisées selon les difficultés rencontrées par les joueurs Les algorithmes que nous avons développés s'appuient sur une modélisation des énigmes du jeu à l'aide de réseaux de Petri, ce qui nous a amenés à concevoir un outil générique d'aide à la construction de ceux-ci. La démarche consiste à exprimer des liens entre des comportements génériques à l’aide d’un langage spécifique et de relations logiques. Ces expressions sont ensuite analysées pour générer automatiquement un réseau de Petri qui modélise tous les parcours possibles. Ce réseau est utilisé pour analyser le parcours du joueur et pour proposer des aides adaptées.

Project Leader : Mathieu Muratet

03/2017

https://github.com/Mocahteam/E-LearningScape

HA-NFV : High Availability Virtual Network Function placement

A Decision Support System (DSS) with graphical interface for Virtual Network Function placement in multi-layer networks under availability objectives.

Project Leader : Stefano SECCI

01/2017

https://ha-nfv.lip6.fr

ULOOF : User-Level Online Offloading Framework

Android application framework allowing any mobile application to be decompiled and recompiled with mobile application method computation offloading features to a remote virtual machine cloning the device. Adaptive decision making allows to offload a method to the VM when computation-energy consumption trade-off is profitable.

Project Leader : Stefano SECCI et Rami LANGAR

01/2017

https://uloof.lip6.fr

BUT4Reuse : Bottom-Up Technologies for Reuse

BUT4Reuse provides a unified framework for mining software artefact variants: Commonality and variability analysis, Feature identification, Feature location, Feature constraints discovery, Feature model synthesis, Reusable assets construction. It is easily extensible and currently supports several artefact types: Java, C, EMF Models, Textual files, File structures, JSON and CSV files, and much more.

Project Leader : Tewfik ZIADI

01/2017

https://but4reuse.github.io

Puck : Puck

Puck est un outil de refactoring de logiciels en Java qui détecte et casse les dépendances nuisibles. Les développeurs peuvent planifier leur refactoring sur un graphe de dépendances et l'appliquer à leur code automatiquement. Puck est encore un prototype de recherche.

Project Leader : Mikal ZIANE

10/2016

https://pages.lip6.fr/puck/

FYFY : FamilY For unitY

FYFY (FamilY For unitY) est une bibliothèque permettant d'intégrer à la plateforme de développement de jeu vidéo Unity le formalisme Entity-Component-System. Ce projet est le prolongement du travail de thèse de Bruno Capdevilla qui avait développé le framework Genome en As3.

Project Leader : Mathieu MURATET

06/2016

https://github.com/Mocahteam/FYFY

SPRED : SPRing EDitor

SPRED est un éditeur de niveau pour le moteur de jeu Spring Engine utilisé par Prog&Play

Project Leader : Mathieu MURATET

06/2016

https://www.irit.fr/ProgAndPlay/

MAGAM : Multi-Aspect Generic Adaptation Model

MAGAM est un modèle générique basé sur un calcul matriciel permettant d'adapter des activités d'apprentissage selon plusieurs aspects (pédagogique, didactique, ludique, motivationnel, etc.).

Project Leader : Vanda LUENGO et Baptiste MONTERRAT

03/2016

https://github.com/Mocahteam/MAGAMmanager

tryalgo : Basic and advanced algorithms and datastructures

Cette bibliothèque comporte des implémentations de plusieurs algorithmes et structures de données pour de nombreux problèmes de graphes, de séquences et de géométrie.

Ces algorithmes sont expliqués dans le livre : Programmation efficace - les 128 algorithmes qu’il faut avoir compris et codés en Python au cours de sa vie.

Project Leader : Christoph DÜRR

03/2016

https://jilljenn.github.io/tryalgo/

VBPMN : Framework for the Verification of BPMN processes

VBPMN supports formal modelling and automated analysis of business processes using formal verification tools. It features a web interface for comparing BPMN 2.0 models.

Project Leader : Pascal POIZAT

01/2016

https://pascalpoizat.github.io/vbpmn/

LEA4PA : LEarning Analytics for Adaptation and Personnalisation

Le projetLEarning Analytics for Personalization and Adaptation a pour objectif de proposer, à destination des décideurs (ensei-gnants, apprenants, ..), des algorithmes et des visualisations permettant des analyses du com-portement de l’étudiant pour l’adaptation et la remédiation. Il s’applique à plusieurs niveaux d’enseignement. Pour le niveau collège, la recherche est menée dans le cadre d’une collaboration soutenue par la direction du numérique pour l’éducation (MEN). Dans ce contexte, nous proposons des analyses (descriptives et diagnostiques) des compétences des apprenants en algèbre, ainsi que des visualisations, l’objectif étant d’assister l’enseignant dans l’adaptation des activités[4].Pour l’enseignement supérieur, la recherche est menée en s’appuyant sur la plateforme LA-PAD développée par CAPSULE (centre d’innovation pédagogique de Sorbonne Université).Dans ce contexte, nous nous intéressons à comprendre les parcours des apprenants à partir de techniques d’analyse séquentielle et de règles d’association.

Project Leader : Vanda LUENGO et Amel YESSAD

01/2016

MySlice v2 : Web portal to reserve and manage heterogeneous ICT resources from federated platforms

Portail web pour la réservation et la gestion de resources informatique hétérogènes hébergées par une fédération de plateformes

Project Leader : Serge FDIDA

01/2016

http://gitlab.noc.onelab.eu/onelab/myslice

F-Interop : Remote interoperability testing services for IoT devices

Services de tests d'interopérabilité à distance pour les objets connectés (IoT)

Project Leader : Serge FDIDA

01/2016

http://f-interop.eu

Marmote : A Markov Modeling Platform

Marmote est une plate-forme de programmation pour la construction et la résolution de modèles de Markov avec des espaces d'état discrets. Elle se compose d'une API C++ et d'une bibliothèque de modèles prédéfinis.

Il est accompagné d'une API d'application pour les processus de décision de Markov : MarmoteMDP.

Il est accompagné également d'une API sous Python qui encapsule le code C++.

Project Leader : Emmanuel Hyon

01/2016

https://marmote.gitlabpages.inria.fr/marmote/

PROMISE : PRecision OptiMISE

PROMISE est un logiciel permettant de déterminer automatiquement la précision adéquate des variables dans un code numérique.

Project Leader : Fabienne JEZEQUEL

01/2016

http://promise.lip6.fr

piexplorer : an explicit state-space generation tool and a model-checker for the Pi-calculus

La génération d'espace d'états pour le pi-calcul est un problème complexe. Il n'existe à ce jour que deux outils offrant cette fonctionalité : le laboratoire HAL et pi-explorer. Ce dernier repose sur une sémantique symbolique beaucoup plus économe que la sémantique précoce exploitée par HAL. Un vérificateur de modèle est associé à l'outil, mais il est possible d'utiliser d'autres outils à partir du graphe d'état généré en sortie de pi-explorer. Ces outils sont basés sur des travaux récents de l'équipe APR (les pi-graphes) en collaboration avec l'université d'Evry et l'université libre de Bruxelles.

Project Leader : Frédéric PESCHANSKI

09/2015

https://github.com/fredokun/piexplorer

LaTTe : a laboratory of type theory experiments

LaTTe est un assistant de preuve basé sur la théorie des types. La caractéristiques principale de LaTTe est d'être conçu comme une bibliothèque (contrairement à la plupart des assistants conçus comme des outils indépendants) complètement intégrée dans le langage et l'écosystème Clojure. Cela permet la diffusion et l'échange de contenus mathématiques élaborés de façon collaborative sur Internet. L'assistant fournit également un langage à domaine spécifique pour les preuves déclaratives, basé sur le style "fitch" de preuves pour la déduction naturelle. L'outil est développé au sein de l'équipe APR en collaboration avec l'équipe Whisper (Pierre-Evariste Dagand).

Project Leader : Frédéric PESCHANSKI

03/2015

https://github.com/fredokun/LaTTe

SPARQL on Spark : SPARQL query processing with Apache Spark

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.

Project Leader : Hubert NAACKE

01/2015

http://www-bd.lip6.fr/wiki/en/site/recherche/logiciels/sparqlwithspark

MOOC backend : Backend server handling network measurement requests coming from a MOOC

Serveur permettant de gérer les requêtes de mesures réseau provenant d'un MOOC

Project Leader : Timur FRIEDMAN

01/2015

https://github.com/onelab-eu/myslice-mooc

ITS-Tools : Instantiable Transition System Tools

ITS Tools est un model-checker symbolique acceptant en entrée un large éventail de formalismes et vérifiant des propriétés de sûreté, mais aussi des formules LTL et CTL.

Project Leader : Yann THIERRY-MIEG

01/2015

https://lip6.github.io/ITSTools-web/

PENDULUM : OCaml syntax extension dedicated to the programming of reactive systems on the Web

Pendulum is a language dedicated to the programming of reactive systems on the Web. It has a powerful expressivity to describe synchronous concurrent systems communicating with broadcast signals. Its constructions and implementation are mostly based on Esterel. The language is embedded in OCaml as a syntax extension. It allows the programmer to describe reactive machines as OCaml values, and run them on signal arguments. The execution of concurrency in pendulum is completely sequential and the scheduling is static. (similar work and inspiration)

Project Leader : Rémy EL SIBAE

11/2014

https://github.com/remyzorg/pendulum

Laalys : Laalys

Laalys (Learner Activity AnaLYser) est un logiciel qui combine une approche basée sur l'expertise humaine et une approche basée sur l'analyse de données pour annoter et décrire le comportement d'un joueur dans le cadre d'un jeu sérieux. DEs descripteurs pédagogique et sémantique sont générées pour caractériser les actions d'un joueur. La première version de Laalys a été réalisée dans le cadre de la thèse de P. Thomas et adaptée aux jeux sérieux de type "étude de cas". La dernière version de Laalys est adaptée à des jeux sérieux hautement intéractifs et possédant de grands espaces d'états. .

Project Leader : Amel YESSAD et Mathieu MURATET

02/2014

ExBLAS : Exact Basic Linear Algebra Subprograms

ExBLAS fournit une version performante des algorithmes fondamentaux d'algèbre linéaire dont les résultats sont précis et reproductibles.

Project Leader : Stef GRAILLAT

01/2014

https://github.com/riakymch/exblas

NFD : Named data network forwarder

NFD is a network forwarder that implements and evolves together with the Named Data Networking (NDN) protocol. The main design goal of NFD is to support diverse experimentation of NDN technology. The design emphasizes modularity and extensibility to allow easy experiments with new protocol features, algorithms, and applications. NFD is an open and free software package licensed under GPL 3.0 license and is the centerpiece of our committement to making NDN’s core technology open and free to all Internet users and developers.

Project Leader : Giovanni PAU

12/2013

http://named-data.net/doc/NFD/current/overview.html

VerChor : Framework for the Verification of Choreographies

VerChor enables you to design correct distributed systems following the choreography-based developement approach. Just model the system interaction protocol in your favorite language and let VerChor check for its realizability and retrieve peer interaction skeletons, or let it generate peer controllers to ensure the conformance to the system specification of a set of peers you want to reuse !

Project Leader : Pascal POIZAT

01/2013

https://pages.lip6.fr/Pascal.Poizat/VerChor/

CarFi : Enabling V2X with Wifi

CarFi enables a moving car to connect and communicate with existing WiFi infrastructures. CarFi has been designed to facilitate connected car services at a fraction of the cost. The software is PRIVATE and the ideas are protected by a patent application.

Project Leader : Giovanni PAU

01/2013

http://www.carfi.mobi

BCM4Java : Basic Component Model for Java

Ce projet est une implantation d'un modèle de programmation par composants répartis en Java (20.000 lignes de code et de documentation environ à ce jour, sous GitHub). Il propose les principaux concepts de l'approche à base de composants : composants logiciels, interfaces de composants, ports exposant les interfaces requises et offertes par les composants, et connecteurs explicites. Utilisant la technologie Java RMI, il permet une programmation répartie grâce au déploiement de composants sur différentes machines virtuelles Java (s'exécutant sur différents ordinateurs) et aux appels inter-composants via RMI. Débuté dans le cadre du projet de recherche ANR SALTY où il a permis de développer une application déployant 10.000 composants répartis, ce logiciel a été utilisé par quelques centaines d'étudiants et il l'est toujours d'abord dans le cadre du cours de master 2 ALASCA depuis 2014, puis dans le cadre du cours de master 1 Composants depuis 2019.

Project Leader : Jacques MALENFANT

11/2012

https://github.com/malenfantj/BCM4Java

SFA : API to federate platforms

API pour la fédération de plateformes

Project Leader : Serge FDIDA

01/2012

http://sfawrap.info

BOM : Block-o-Matic!

Block-o-Matic est un algorithme de segmentation de pages Web basé sur une approche hybride pour la segmentation de documents numérisés et la segmentation de contenu à base visuelle. Une page Web est associée à trois structures: l'arborescence DOM, la structure de contenu et la structure logique. L'arborescence DOM représente les éléments HTML d'une page, la structure géométrique organise le contenu en fonction d'une catégorie et de sa géométrie et enfin la structure logique est le résultat de la cartographie de la structure du contenu sur la base du sens humain. Le processus de segmentation est divisé en trois phases: l'analyse, la compréhension et la reconstruction d'une page Web. Une méthode d'évaluation est proposée afin d'effectuer l'évaluation des segmentations de pages Web sur la base d'une vérité de terrain de 400 pages classées en 16 catégories. Un ensemble de mesures est présenté en fonction des propriétés géométriques des blocs. Des résultats satisfaisants sont obtenus en comparaison avec d'autres algorithmes suivant la même approche.

Project Leader : Andrès SANOJA

01/2012

http://www-poleia.lip6.fr/~sanojaa/BOM/

AbSolute : AbSolute

AbSolute est un solveur de contraintes basé sur les domaines abstraits.

Il implémente la méthode de résolution présenté dans l'article : Marie Pelleau, Antoine Miné, Charlotte Truchet, Frédéric Benhamou, Constraint Solver based on Abstract Domains, 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Rome, Italie, 2013 [Article]

Ce solveur peut résoudre des problèmes continus, discrets et mixtes (contenant des variables entières et réelles) et propose des techniques permettant de traiter aussi bien les contraintes linéaires que non-linéaires. La méthode de résolution prend en compte les erreurs d'arrondi et calcule des approximations flottantes sures des solutions réelles d'un problème. AbSolute utilise Apron, une librairie Ocaml de domaines abstraits, qui permet de résoudre des problèmes à l'aide d'autre domaines abstraits que les intervalles.

Project Leader : Marie PELLEAU

11/2011

https://github.com/mpelleau/AbSolute

Arbogen : a fast uniform random tree generator

Arbogen est un générateur aléatoire uniforme de structures arborescentes. L'outil accepte en entrée un fichier de grammaire décrivant un structure arborescente (ex.: arbres binaires, abres 2-3-3, graphes séries-parallèles, etc.) ainsi qu'un intervalle de taille (ex.: arbres de taille 1000+-100). Depuis la grammaire un ou plusieurs arbres acceptés par la grammaire et dans l'intervalle considéré sont générés. Cette génération se fait avec une garantie d'uniformité, ce sont donc des arbres "moyens" dans la taille obtenue. L'outil utilise des algorithmes avancés de génération de Boltzmann, faisant suite à des travaux reconnus de l'équipe APR (in the realm of ANR Magnum 2010-2014).

Project Leader : Frédéric PESCHANSKI

10/2011

https://github.com/fredokun/arbogen

SPOC : Strem Processing with OCaml

SPOC is a set of tools for GPGPU programming with OCaml.

The SPOC library enables the detection and use of GPGPU devices with OCaml using Cuda and OpenCL. There is also a camlp4 syntax extension to handle external Cuda or OpenCL kernels, as well as a DSL (called Sarek) to express GPGPU kernels from the OCaml code.

Project Leader : Mathias BOURGOIN

09/2010

http://mathiasbourgoin.github.io/SPOC/

SAM : Stochastic Arithmetic in Multiprecision

SAM est une bibliothèque qui permet d'estimer et de contrôler la propagation des erreurs d'arrondi dans les programmes en précision arbitraire.

Project Leader : Fabienne JEZEQUEL

01/2010

http://www-pequan.lip6.fr/~jezequel/SAM

WiPal : IEEE 802.11 traces manipulation software

WiPal is a piece of software dedicated to IEEE 802.11 traces manipulation. It comes as a set of programs and a C++ library. A distinctive feature of WiPal is its merging tool, which enables merging multiple wireless traces into a unique global trace. This tool works offline on PCAP traces that do not need to be synchronized. WiPal also provides statistics extraction and anonymization tools, and its authors plan to extend it. WiPal’s key features are flexibility, ease of use, and efficiency.

Project Leader : Marcelo DIAS DE AMORIM

04/2009

http://crawdad.org/tools/process/pcap/WiPal/20090422/

Prog&Play : Prog&Play

Prog&Play est une bibliothèque de fonctions pour les jeux de Stratégie Temps Réel (STR). Elle permet au joueur de programmer de manière simple et intéractive les entités virtuelles d'un STR. Actuellement, le système Prog&Play est intégré au STR multijoueur Kernel Panic. Le système Prog&Play, combiné au jeu de STR Kernel Panic, permet la mise en oeuvre de jeux sérieux centrés sur la pratique de la programmation informatique.

Project Leader : Mathieu MURATET

01/2008

http://progandplay.lip6.fr

WScout : Lightweight PCAP file visualizer.

WScout provides a PCAP traces visualizer that is able to work with huge traces (>10 GiB). Its goals are speed and low memory requirements. Despite its design being protocol-agnostic, it currently handles only Prism and IEEE 802.11 headers, hence its name.

Project Leader : Marcelo DIAS DE AMORIM

09/2007

http://crawdad.org/tools/analyze/pcap/WScout/20070912/

Paris Traceroute : Paris Traceroute

Version améliorée de l'outil classique pour tracer des routes dans internet

Project Leader : Timur FRIEDMAN

01/2006

https://github.com/libparistraceroute

PNML Framework est l'implémentation prototype du standard ISO/IEC-15909 (partie 2), le format d'échange normalisé pour les réseaux de Petri. L'objectif principal de PNML est d'aboutir à l'interopérabilité des outils basés sur les réseaux de Petri. PNML Framework est conçue pour implémenter le standard au fur et à mesure de son élaboration, afin d'en mesurer la faisabilité et de servir de référecne pour es outils de la communauté. Il propose une API de manipulation permettant de créer, sauver, charger et parcourir des réseaux de Petri au format PNML.

Project Leader : Fabrice KORDON

04/2005

http://pnml.lip6.fr

CORIOLIS : Platform for physical synthesis of integrated circuits

Coriolis est une plate-forme logicielle pour la recherche d'algorithmes, le développement d'outils et l'évaluation de nouveaux flots de conception physique VLSI. Les procédés technologiques actuels, nanométriques, posent de nouveaux défis aux flots de CAO. Les recherches académiques concernent souvent la résolution de problèmes trop spécifiques, indépendemment d'autres algorithmes, faute de pouvoir inter-opérer avec eux. Or il est capital de pouvoir évaluer les interactions entre les différents outils au sein d'un flot complet de conception. La plate-frome CORIOLIS, conçue en C++, est faite pour permettre l'inter-opérabilité des différents briques logicielles qui l'utilisent. Elle propose actuellement dessolutions aux problèmes de partitionnement, de placement et routage de circuits numériques, en technologie nanométrique.

Project Leader : Jean-Paul CHAPUT

01/2004

https://www.lip6.fr/coriolis

CAIRO : Analog IP Design

L'objectif du projet CAIRO est de développer des méthodes et des outils autorisant une réutilisation des cellules analogiques et une capitalisation de connaissances du concepteur sous forme des cellules IP (Intellectual Property) portables d’une technologie à l'autre et d’un jeu de spécifications à l'autre. Le langage CAIRO+, ensemble de fonctions C++, est un langage de création d’IP analogiques permettant de structurer, de formaliser et d’automatiser en grande partie le flot de conception analogique. Il est utilisé pour créer une procédure appelée «générateur» pour une cellule analogique. A l'étape actuelle d'avancement du projet, la structure électrique de la cellule (i.e. le schéma électrique non dimensionné) est figée par le concepteur. Le générateur doit permettre un dimensionnement des composants de la cellule (définition de la taille des transistors, des capacités etc.) et de synthétiser le layout – le tout en fonction des spécifications de la cellule et des paramètres technologiques. L'écriture du générateur de la cellule est à la charge du concepteur, notamment, la partie qui concerne le dimensionnement électrique du circuit. Un des points forts du langage CAIRO+ est, sans doute, la possibilité de synthétiser le layout d'une manière quasi-automatique, à partir du schéma électrique dimensionné – la fonction de génération du layout fait partie des modules «natifs» du langage. De plus, le dimensionnement électrique peut prendre en compte les éléments parasites du layout (nous disons «peut», car tout dépend de la volonté du concepteur qui définit la procédure de dimensionnement). Dans ce cas, plusieurs cycles «dimensionnement de la cellule – synthèse du layout» peuvent être nécessaires. Un des pôles d'intérêt de ce groupe est la conception de modulateurs sigma-delta temps continu. Dans cette activité nous nous attachons à capitaliser l’effort de conception en développant des méthodes et des outils permettant une réutilisation des résultats. La structure complexe des modulateurs, incluant un grand nombre de cellules de fonctionnalité identique mais de spécifications différentes (telles que GmC, amplificateurs), offre un contexte approprié pour l’application de la méthodologie implémentée dans CAIRO+.

Project Leader : Marie-Minerve LOUËRAT

01/2004

DDD : Library for manipulation of Data Decision Diagrams

La libDDD est une bibliothèque de manipulation des Data Decision Diagrams et des Hierarchical Set Decision Diagrams. Elle supporte flexiblement des types de données complexes et las algorithmes de "saturation", offrant à ses utilisateurs des performances au sommet de l'état de l'art. Cette bibliothèque C++ est distribué sous les termes de la LGPL de Gnu.

Project Leader : Yann THIERRY-MIEG

01/2001

http://ddd.lip6.fr

Salammbo : Construction and Use of Fuzzy Decision Trees

Salammbô est un logiciel d'apprentissage automatique permettant de construire des arbres de décision flous à partir d'un ensemble d'exemples (ensemble d'apprentissage). Il permet de tester différents types de paramètres : mesures de discrimination (entropie floue, mesure d'ambiguïté, etc.), t-normes/t-conormes, critères d'arrêt, etc. De plus, il met en œuvre une méthode automatique pour construire des ensembles flous pour des variables numériques à partir d'un ensemble de valeurs numériques (précises).

Project Leader : Christophe MARSALA

05/2000

JADE : The Java Agent DEvelopment framework

JADE (Java Agent DEvelopment Framework) is an open source platform for peer-to-peer agent based applications.

JADE simplifies the implementation of multi-agent systems through a middleware that complies with the FIPA specifications for interoperable intelligent multi-agent systems.

JADE provides a simple yet powerful task execution and composition model, peer-to-peer agent communication based on asynchronous message passing, a yellow pages service supporting publish subscribe discovery mechanism and many other advanced features that facilitates the development of distributed systems.

A JADE-based system can be distributed across the internet and can tranparently deploy agents on Android and J2ME-CLDC MIDP 1.0 devices. The platform configuration as well as the agent number and locations can be changed at run-time, as and when required.

Project Leader : Cédric Herpson

01/2000

https://jade-project.gitlab.io/

CPN-AMI est un environnement conçu sur FrameKit: une plate-forme logicielle d'intégration permettant un couplage rapide d'outils de provenance diverses. CPN-AMi est ainsi l'assemblage le plus complet d'outils de vérifications à partir de réseaux de Petri. Ces outils ont été développés dans le cadre des travaux de SRC ou par des partenaires universitaires (Université de Turin, Université d'Helsinki, Bell-Labs, Université de Munich, Université Humbolt à Berlin). CPN-AMI est composé d'un serveur d'outils et d'une interface utilisateur déporté à laquelle on se connecte.

Project Leader : Fabrice KORDON

12/1994

https://www.lip6.fr/cpn-ami

Système d'objets à la CLOS pour Scheme

Project Leader : Christian QUEINNEC

01/1993

http://lip6.fr/Christian.Queinnec/WWW/Meroon.html

CADNA : Control of Accuracy and Debugging for Numerical Application

CADNA est une bibliothèque qui permet de faire du calcul scientifique sur ordinateur en estimant et contrôlant la propagation des erreurs d'arrondi

Project Leader : Fabienne JEZEQUEL

01/1992

https://www-pequan.lip6.fr/cadna/

Macao : Modélisation Analyse et Conception Assistées par Ordinateur

Macao est un logiciel générique de dessin de graphes. Avec une interface utilisateur intuitive, il permet de dessiner très facilement des graphes. Macao est aussi l'interface une interface utilisateur de FrameKit, une plate-forme dédiée au prototypage et à la validation de systèmes complexes.

Project Leader : Jean-Luc MOUNIER

09/1987

https://www.lip6.fr/macao

aGrUM : a Graphical Unified Model

aGrUM est une librairie en C++ de manipulation de modèles graphiques. Son spectre est assez large puisqu'elle est conçue pour faire de l'apprentissage (de réseaux bayésiens par exemple), de la planification (FMPDs) ou bien encore de l'inférence (réseaux bayésiens, GAI, diagrammes d'influence).

Project Leader : Christophe GONZALES & Pierre-Henri WUILLEMIN

https://agrum.org

FoCaLize : FoCaLize

Atelier de développement intégré pour les logiciels critiques

Project Leader : Thérèse HARDIN

http://focalize.inria.fr

WEB-R : Web-R, the complete memory of my Web

Web-R, un outil non-intrusif et rapide d’enregistrement qui réalise un stockage complet et systématique des pages web de l’utilisateur et de sa navigation.

Project Leader : Alain LIFCHITZ

RAGLib : A Library for Real Algebraic Geometry

Cette bibliothèque, implantée en Maple, contient quelques fonctionnalités pour l'étude des solutions réelles des systèmes polynomiaux de dimension positive.

Project Leader : Mohab SAFET EL DIN

http://www-calfor.lip6.fr/~safey/RAGLib

VideoScm2003 : VideoScm2003

Logiciel d'accompagnement pour l'apprentissage et la programmation récursive en scheme et la notion de processus d'évaluation.

Project Leader : Maryse PELLETIER et Michele SORIA

http://www-ari.ufr-info-p6.jussieu.fr/RESSOURCES/cederoms.htm

Epsilon : Epsilon

Epsilon est une bibliothèque de fonctions implentée en Maple et Java dédiée a l'élimination polynomiale et aux applications géométriques. Elle est composée de 8 modules et contient plus de 70 fonctions.

Project Leader : Dongming WANG

http://www-calfor.lip6.fr/~wang/epsilon/

DARX est une plate-forme d'exécution générique pour systèmes multi-agents développée conjointement entre l'équipe OASIS du LIP6 et SRC. DARX permet de fiabiliser par réplication les agents. Outre sa généricité, sa principale originalité est (1) la capacité à pouvoir changer dynamiquement de stratégies de réplication en fonction des contraintes applicatives et (2) son adaptation à la grande échelle en adoptant une architecture hiérarchique. DarX est implanté au-dessus de Java-RMI.

Project Leader : Pierre SENS

VVM : Virtual Virtual Machine

Le nombre toujours croissant de domaine d'application émergent entraîne un nombre croissant de solutions ad-hoc, rigides et faiblement interopérables. Nous proposons une plateforme pour la construction d'applications et d'environnement d'exécution flexibles et interopérables appellée la Machine Virtuelle Virtuelle. Plusieurs logiciels sont disponibles en libre sur Internet autour de la MVV: la RVM (Recursive Virtual Machine) le CCG (Compiler Compiler Generator) CCG a été notamment utilisé par le SUN Research Lab dans le cadre de la KVM.

Project Leader : Bertil FOLLIOT

SPOT : Spot Produces Our Traces

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.

Project Leader : Denis POITRENAUD

http://spot.lip6.fr/

LfP : Language for Prototyping

Il s'agit d'un langage de spécification de systèmes répartis à partir duquel nous travaillons pour générer automatiquement des spécifications formelles et des programmes. Le compilateur de ce langage a été écrit et intégré dans la plate-forme FrameKit (à coté de l'environnement CPN-AMI pour permettre un couplage et exploiter les outils de vérification). Ce langage et son compilateur sont à l'origine de notre participation dans le projet RNTL MORSE

Project Leader : Fabrice KORDON

Outil de programmation littéraire

Project Leader : Christian QUEINNEC

http://lip6.fr/Christian.Queinnec/WWW/l2t.html