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

    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

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

  University of York
  International Joint Project MoBasT
  LSV, ENS Cachan

Recent Ph.D. dissertations & faculty habilitations
  Traduction certifiée et mécanisée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée
  Development and verification of arbitrary-precision integer arithmetic libraries
  Extensions of the backward reachability algorithm in the context of model checking modulo theories

Quantum at LRI

4 February 2020 09h00

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