Equipes (Equipes) - Laboratoire de Recherche en Informatique

Vérification d'Algorithmes, Langages et Systèmes (VALS)

The VALS team works in the Area of (V)erification, (V)alidation of (A)lgorithms, (L)anguages and (S)ystems, right in the heart of the scientific field called "Formal Methods". The main objectives of the team are:
- making verification an easier to use, more wide-spread technology,
- pushing the limits of formal verification in non-standard application domains
- advancing the technology of interactive and automated theorem provers
- improving foundations by verifying languages, systems, and tools
- developing combinations of formal test and proof techniques
- developing combinations of proofs and probability.
http://fortesse.lri.fr/
http://toccata.lri.fr/

Site web de l'equipe

Composition de l'équipe
  Responsable
    CONTEJEAN Evelyne

  Membres permanents
    AIT-SADOUNE Idir
    ARRIGHI Pablo
    BALABONSKI Thibaut
    BENZAKEN Véronique
    BOLDO Sylvie
    BOULANGER Frédéric
    CONTEJEAN Evelyne
    FILLIÂTRE Jean-Christophe
    JOURDAN Jacques-Henri
    KELLER Chantal
    LONGUET Delphine
    MANDEL Louis
    MARCHÉ Claude
    MELQUIOND Guillaume
    NGUYEN Kim
    PASKEVYCH Andriy
    PAULIN-MOHRING Christine
    TAHA Safouan
    VALIRON Benoît
    VOISIN Frédéric
    WOLFF Burkhart
    YE Lina
    ZAIDI Fatiha

Activités de recherche
  Démonstration automatique, SMT et applications
  Formalisation et preuves de programmes numériques
  Formalisation de langages (de spécification et de programmation) dans les assistants de preuve
  Langages et systèmes centrés données
  Test formel basé sur les modèles
  Vérification déductive de programmes

Equipes-projets Inria communes
  Toccata

Logiciels et brevets
  Alt-Ergo : Démonstrateur automatique Alt-Ergo
  ocamlgraph : bibliothèque de graphes pour Ocaml
  Krakatoa : Outil Krakatoa de vérification de programmes Java
  Lucid Synchrone : Lucid Synchrone
  Program : Program : un langage de programmation avec types dépendants dans Coq
  AuGuSTe : Test statistique de programmes C
  CiME : CiME: une boîte à outils pour la démonstration automatique.
  CDuce : CDuce an XML centric Functional Programmimg Language
  HOL-TestGen : Générateur de tests à partir de spécifications HOL
  HOL-OCL : Un systeme de preuve pour UML/OCL
  Le Système HOL-Z : Un système de preuve pour la Méthode Z
  Frama-C : Framework for Modular Analysis of C
  Gappa : Outil Gappa de certification de programmes numériques
  Coq.Interval : Bibliothèque Coq.Interval de preuve automatique de bornes sur des expressions à valeurs réelles
  RUKIA : Random Uniform walK In Automata
  Coq.FP2 : Coq.FP2
  ALEA : ALEA : A library for reasoning on random algorithms in Coq
  Coccinelle : Coccinelle
  Flocq Library : Flocq Library
  Isabelle/HOL : Isabelle/HOL
  CUBICLE : A PARALLEL SMT-BASED MODEL CHECKER FOR PARAMETERIZED SYSTEMS
  The Coquelicot library : The Coquelicot library
  Pff library : Pff library
  CFML : Program Verification for ML through Characteristic Formula
  Datacert : DataCert: A coq library for Data Intensive Languages and Systems Certification
  Coq : L'assistant de preuve Coq
  SMTCoq : Plug-in de communication entre Coq et prouveurs externes
  Iris : Une logique de séparation d'ordre supérieur implémentée dasn l'assistant de preuve Coq
  BOLDR : Query Intermediate Representation Library
  Pactole : Formalisation en Coq de modèles et d'algorithmes d'essaims de robots mobiles.

Collaborations
  Université de York
  MBTSEC
  CEA-LIST
  International Joint Project MoBasT
  System X FSF
  LSV, ENS Cachan
  AdaCore SAS

Thèses et habilitabions récentes
  Traduction certifiée et mécanisée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée
  Développement et vérification de bibliothèques d'arithmétique entière en précision arbitraire
  Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories