Forge
Logiciels APR
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
Arbogen : un générateur aléatoire uniforme de grands arbres
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
LaTTe : un laboratoire d'expériences pour la théorie des types
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
MOPSA analyzer : Analyseur statique MOPSA
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
OMicroB : OCaml sur microcontrôleurs
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
PENDULUM : Extention de syntaxe OCaml pour la préogrammation de systèmes reéactif sur le 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
piexplorer : un générateur d'espace d'état explicite et un vérificateur de modèle pour le Pi-calcul
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
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
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
