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/
Group leader
CONTEJEAN Evelyne
Faculty
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
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 Toccata
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
CUBICLE: A PARALLEL SMT-BASED MODEL CHECKER FOR PARAMETERIZED SYSTEMS
The Coquelicot library: The Coquelicot library
Pff library: Pff library
CFML: CFML
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.
Collaborations University of York MBTSEC CEA-LIST 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
