Avant tout, nous sommes des chercheurs.
Fondés par des chercheurs de l'INRIA, nous publions dans les meilleures conférences mondiales et contribuons aux écosystèmes open source. La recherche est notre identité.
Dernières nouvelles du labo
Legacy Systems: Your Greatest Undetected IT Risk (and How to Master It)
A system that has been running for fifteen years without a major incident is not necessarily reliable. Discover why legacy systems represent an invisible risk and how to manage it.
Fabrice Le Fessant on Digital Independence and Technological Sovereignty
Fabrice Le Fessant discusses digital sovereignty, open source, and building long-term European tech companies in an interview with La Jaune et la Rouge.
Publications de recherche récentes
Cross-Language Symbolic Runtime Annotation Checking
Zhicheng Hui, Léo AndrèsTail Modulo Cons, OCaml, and Relational Separation Logic
Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel SchererL'explication par la paresse: Techniques d'évaluation hybrides à des fins d'explication de calculs
Louis GesbertRelational Abstractions Based on Labeled Union-Find
Dorian Lesbre, Matthieu Lemerre, Hichem Rami Ait-El-Hara, François BobotStorable types: free, absorbing, custom
Basile Clément, Gabriel SchererUne expertise approfondie, du compilateur au déploiement
OCaml
Programmation fonctionnelleNotre langage fondateur. Nous développons les outils essentiels dont le compilateur Flambda2 et le gestionnaire opam.
Rust
Programmation systèmeProgrammation système sûre pour les applications critiques. Nous aidons les équipes à adopter Rust en toute confiance.
C
Bas niveau & EmbarquéExpertise en vérification C et analyse statique. SeaCoral permet la génération automatique de tests pour le code critique.
COBOL
Modernisation legacyNous maintenons GnuCOBOL et éditons SuperBOL Studio, l'IDE COBOL moderne pour migrations souveraines.
WebAssembly
Exécution portableDétection de bugs via Owi, notre boîte à outils d'analyse symbolique WebAssembly (C, Rust, Go, Zig).
Méthodes formelles
Vérification mathématiqueSolveur Alt-Ergo et intégration Frama-C. Nous prouvons mathématiquement la correction des logiciels.
Là où nous repoussons les limites
Vérification formelle
Prouver la correction logicielle par le raisonnement mathématique (solveurs SMT, interprétation abstraite).
Optimisation de compilateurs
Développement de compilateurs haute performance pour OCaml, COBOL et langages dédiés (DSL).
Théorie des langages
Recherche sur les systèmes de types et la sémantique formelle alimentant directement nos outils.
Analyse symbolique
Détection automatique de bugs via l'exploration systématique de tous les chemins d'exécution (Owi).
Ingénierie logicielle
Création de l'infrastructure (gestionnaires de paquets, systèmes de build) rendant les langages utilisables à grande échelle.
Collaborations académiques
