Français Anglais
Accueil Annuaire Plan du site
Home > Groups > Research groups > Verification of Algorithms, Languages and Systems (VALS)
Verification of Algorithms, Languages and Systems (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.

Group Members
  Group leader
    CONTEJEAN Evelyne

    BALABONSKI Thibaut
    BENZAKEN Véronique
    BOLDO Sylvie
    CONCHON Sylvain
    CONTEJEAN Evelyne
    FILLIÂTRE Jean-Christophe
    GAUDEL Marie-Claude
    HILAIRE Thibault
    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

  Non-permanent research staff
    BLOT Valentin
    CLOCHARD Martin
    DAILLER Sylvain
    DECLERCK David
    FAISSOLE Florian
    HACHMAOUI Mohammed
    LOPEZ Julien
    OUFFOUE Georges
    PELLE Robin
    ROUX Mattias



    GALLOT Maëlis
    TOURNEUR Vincent

Research activities
  Automated Proof, SMT and Applications
  Formalisation and Proof of Numerical Programs
  Formalisation of (Specification and Programming) Languages in Proof Assistants
  Data-Centric Languages and Systems
  Formal Model-Based Testing
  Deductive Verification of Programs

Joint Inria project teams

Software & patents
  Alt-Ergo: The Alt-Ergo theorem prover
  ocamlgraph: Ocaml graph library
  Krakatoa: Krakatoa Tool for Java Program Verification
  Lucid Synchrone: Lucid Synchrone
  Program: Program : Programming with Dependent Types in Coq
  AuGuSTe: Statistical Testing of C Programs
  CiME: CiME, a tool box for automated deduction.
  CDuce: CDuce an XML centric Programmimg Language
  HOL-TestGen: A generator of test-data from HOL specifications
  HOL-OCL: A proof system for UML/OCL
  Le Système HOL-Z: The HOL-Z System
  Frama-C: Framework for Modular Analysis of C
  Gappa: Gappa, a tool for certifying numerical applications
  Coq.Interval: The Coq.Interval library for automatically proving bounds of real-valued expressions
  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
  The Coquelicot library: The Coquelicot library
  Pff library: Pff library
  Datacert: DataCert: A coq library for Data Intensive Languages and Systems Certification

  University of York
  International Joint Project MoBasT
  LSV, ENS Cachan

Recent Ph.D. dissertations & faculty habilitations
  Random based testing of C program
  Un système de types pragmatique pour la vérification déductive des programmes
  A Coq Formalization of Relational and Deductive Databases - and Mechanizations of Datalog

Deciding ATL* by Tableaux
Amélie DAVID
10 April 2015 10h00

Formal Proofs of Rounding Error Bounds
Pierre Roux
27 March 2015 10h00

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

Coq, the world's best macro assembler!
Pierre-Évariste Dagand
7 February 2014 10h00

Résultats majeurs
A Coq Formalization of the Relational Data Model
7 April 2014
V. Benzaken, E. Contejean, S. Dumbrava

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
5 July 2012

Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
22 March 2012

Formal firewall conformance testing: an application of test and proof techniques
1 September 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 September 2014
Available online 28 August 2014 DOI: 10.1016/j.tcs.2014.08.012

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

Software & patents