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é.
Nos derniers articles de blog
COBOL Modernization: Should You Migrate or Upgrade Your Tooling?
Is your COBOL a ticking time bomb or your greatest asset? Discover modernization strategies without full rewriting.
Digital Sovereignty: It's Not Where Your Cloud Runs. It's Who Can Read Your Code.
The sovereignty debate has asked the wrong question for a decade. Where your servers sit does not protect you. Being able to read your code does.
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.
Dernières nouvelles du labo
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
01. Vérification formelle
Prouver la correction logicielle par le raisonnement mathématique (solveurs SMT, interprétation abstraite).
02. Optimisation de compilateurs
Développement de compilateurs haute performance pour OCaml, COBOL et langages dédiés (DSL).
03. Théorie des langages
Recherche sur les systèmes de types et la sémantique formelle informant directement les outils que nous construisons.
04. Analyse symbolique
Détection automatique de bugs via l'exploration systématique de tous les chemins d'exécution (Owi).
05. Ingénierie logicielle
Création de l'infrastructure (gestionnaires de paquets, systèmes de build) rendant les langages utilisables à grande échelle.
Collaborations académiques
