Français Anglais
Accueil Annuaire Plan du site
Accueil > Equipes > Toutes les équipes > Vérification d'Algorithmes, Langages et Systèmes (VALS)
Equipes
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/

Composition de l'équipe
  Responsable
    CONTEJEAN Evelyne

  Membres permanents
    BALABONSKI Thibaut
    BENZAKEN Véronique
    BOLDO Sylvie
    CHARGUERAUD Arthur
    CONCHON Sylvain
    CONTEJEAN Evelyne
    FILLIÂTRE Jean-Christophe
    GAUDEL Marie-Claude
    KELLER Chantal
    LONGUET Delphine
    MANDEL Louis
    MARCHÉ Claude
    MELQUIOND Guillaume
    NGUYEN Kim
    PASKEVYCH Andriy
    PAULIN-MOHRING Christine
    VOISIN Frédéric
    WOLFF Burkhart
    ZAIDI Fatiha

  Membres non-permanents
    CLOCHARD Martin
    COQUEREAU Albin
    DAILLER Sylvain
    DECLERCK David
    FAISSOLE Florian
    FUMEX Clément
    HACHMAOUI Mohammed
    LOPEZ Julien
    NGUYEN VAN Hai
    OUFFOUE Georges
    PARREIRA PEREIRA Mario
    PELLE Robin
    ROUX Mattias

  Associés
    IGUERNELALA Mohamed

  Stagiaires
    COSTE Julie
    GALLOT Maëlis
    HERVIOU Yoann
    MARTINS Eunice
    NABILI Samia
    RIEU-HELFT Raphaël

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

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
  Random based testing of C program
  Un système de types pragmatique pour la vérification déductive des programmes
  Formalisation en Coq de Bases de Données Relationnelles et Déductives - et Mécanisation de Datalog

Séminaires
Deciding ATL* by Tableaux
Amélie DAVID
Ven. 10 avril 2015 - 10h00


Formal Proofs of Rounding Error Bounds
Pierre Roux
Ven. 27 mars 2015 - 10h00


ProvenCore: Towards a Verified Isolation Micro-Kernel
Stéphane Lescuyer
Ven. 20 mars 2015 - 10h00


Coq, the world's best macro assembler!
Pierre-Évariste Dagand
Ven. 07 février 2014 - 10h00


Résultats majeurs
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
05 juillet 2012
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. IJCAR 2012

Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
22 mars 2012
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi, CAV 2012

ESOP 2014 : A Coq Formalization of the Relational Data Model
07 avril 2014
V. Benzaken, E. Contejean, S. Dumbrava

Formal firewall conformance testing: an application of test and proof techniques
01 septembre 2014
A Formal Security Policy Model (UPF) is applied to network policies (firewalls, routers, NATs). Derived Rules allow for a proven correct test-generation procedure for these policies.

Test selection for traces refinement, Ana Cavalcanti and Marie-Claude Gaudel
28 septembre 2014
Available online 28 August 2014 DOI: 10.1016/j.tcs.2014.08.012

Testing for refinement in Circus
21 mars 2011
Ana Cavalcanti and Marie-Claude Gaudel, ACTA INFORMATICA Volume 48, Number 2, 97-147, DOI: 10.1007/s00236-011-0133-z

Logiciels et brevets