Nous sommes chercheurs. Ça change tout.
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
Digital Sovereignty: It's Not Where Your Cloud Runs. It's Who Can Read Your Code.
The digital sovereignty debate has been asking the wrong question for a decade. Where your servers are located doesn't protect you. What protects you is your ability to understand, audit, and modify the code running your critical systems.
Software Reliability: Systems Must Not Fail You at the Wrong Time
Discover how to ensure the software reliability of your critical systems and avoid costly outages through independent testing.
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.
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.
Nos domaines de recherche actifs
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 informant directement les outils que nous construisons.
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
