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
    BOULANGER Frédéric
    CONCHON Sylvain
    CONTEJEAN Evelyne
    FILLIÂTRE Jean-Christophe
    GAUDEL Marie-Claude
    HILAIRE Thibault
    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

  Non-permanent research staff
    BECKER Benedikt
    DAILLER Sylvain
    FAISSOLE Florian
    FARINIER Benjamin
    GARCHERY Quentin
    HACHMAOUI Mohammed
    HE Lulu
    HEURTEL Nicolas
    KORNEVA Alexandrina
    LANCO Antoine
    LEE Dongho
    LOPEZ Julien
    MALAK Rehan
    MEVEL Glen
    OUFFOUE Georges
    PELLE Robin
    RIEU-HELFT Raphaël
    ROUX Mattias
    STEINBERG Florian
    TODOROV Vassil
    TUONG Frédéric
    XU Zhaowei

    ZHOU Wenbo

    BLOT Valentin

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

Contracts & grants

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
  SMTCoq: Coq plugin that checks proof witnesses coming from external SAT and SMT solvers
  Coq: The Coq proof assistant
  Iris: A Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq.
  Pactole: Coq formalisation a mobile sensors networks.
  BOLDR: Query Intermediate Representation Library

  University of York
  International Joint Project MoBasT
  LSV, ENS Cachan

Recent Ph.D. dissertations & faculty habilitations
  Formal Verification for Numerical Computations,and the Other Way Around
  Attack Tolerance for Services-based Applications in the Cloud
  Tools and Techniques for the Verification of Modular Stateful Code

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