Contracts and grants

  • ANR DataCert (Coq deep specification of security aware data integration)
    Our research goal is to develop a comprehensive framework that handles the fundamental problems underlying security aware data integration and sharing, to achieve a paradigm shift in the design and implementation of security aware data integration systems. To fill the gap between both worlds, we will strongly rely on deep specifications and proven correct software. We will develop formal models that will eventually lead to highly reliable technology needed to integrate distributed data while controlling the disclosure of private or confidential information.
    Team members involved: É. Contejean (national and local coordinator), V. Benzaken
    In collaboration with CRIStAL (University Lille 1), LIRIS (University Claude Bernard - Lyon ) and LRI (CNRS - University Paris Sud and Université Paris Saclay project leader)
    Starting: January 2016. Duration: 60 months.
  • Sponsored Research Grant - Oracle (Deep Integration of Programming Languages and Databases with Truffle)

    Team members involved: V. Benzaken (local coordinator), K. Nguyen (local coordinator), J. Lopez.
    In collaboration with G. Castagna PPS-LIAFA (University Paris-Diderot)
    Starting: October 2015. Duration: 48 months.
  • ANR CoLiS (Correction of Linux Scripts)
    This project aims at applying techniques from deductive program verification and analysis of tree transformations to the problem of analyzing shell scripts, in particular those that are used in software installation.
    Team members involved: Claude Marché (local coordinator), Jean-Christophe Filliâtre, Kim Nguyen, Andrei Paskevich.
    In collaboration with PPS-LIAFA (University Paris-Diderot, project leader) and Links team of Inria Lille
    Starting: October 2015. Duration: 48 months.
  • ANR AJACS (JavaScript applications: certified analyses and security)
    Team member involved: Arthur Charguéraud.
    In collaboration with Inria Rennes, Inria Paris-Rocquencourt, and Inria Sophia-Antipolis.
    Starting: December 2014. Duration: 42 months.
  • ProofInUse (ANR LabCom programme)
    Deduction verification tools for industry users of Ada
    Team members involved: Claude Marché (coordinator), Jean-Christophe Filliâtre, Andrei Paskevich.
    In collaboration with AdaCore S.A.
    Starting: April 2014. Duration: 36 months.
  • ANR VERASCO (formal verification of static analyzers and compilers)
    Team members involved: Sylvie Boldo, Guillaume Melquiond.
    In collaboration with Inria Rocquencourt, Airbus, University of Rennes 1, Verimag.
    Starting: January 2012. Duration 48 months.
  • ANR FastRelax (fast and reliable approximations of numerical values)
    Team members involved: Sylvie Boldo, Guillaume Melquiond.
    In collaboration with ENS Lyon, Inria Saclay, LAAS, UMPC, Inria Sophia-Antipolis.
    Starting: October 2014. Duration: 60 months.
  • Standardization of interval arithmetic IEEE-1788 (Inria D2T)
    Team member involved: Guillaume Melquiond.
  • ANR BWARE (a proof-based mechanized plate-forme for the verification of B proof obligations)
    Team members involved: Sylvain Conchon, Evelyne Contejean, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich.
    In collaboration with Cedric (CNAM), Inria Paris-Rocquencourt, Mitsubishi Electric R&D Centre Europe, ClearSy, OCamlPro.
    Starting: September 2012. Duration: 48 months.
  • ANR CAFEIN (combining analyses for the study of numerical invariants)
    Team members involved: Sylvain Conchon.
    In collaboration with CEA List, ENSTA ParisTech, Inria Saclay (EPI MaxPlus), ONERA DTIM, Prover Technology, Rockwell Collins France, Université de Perpignan Via Dormitia.
    Starting: February 2013. Duration: 36 months.
  • ANR SOPRANO (novel automatic solver for program analysis)
    Team members involved: Sylvain Conchon, Evelyne Contejean, Guillaume Melquiond.
    In collaboration with Adacore, CEA List, Inria Rennes, OcamlPro.
    Starting: October 2014. Duration: 42 months.
  • STIC-AmSud Project -DATE (Distributed Diagnosability and Testability of Faulty Systems)
    Team members involved: Delphine Longuet, Fatiha Zaidi.
    In collaboration with FAMAF (Universidad Nacional de Cordoba, Argentina), UACH (Universidad Austral de Chile, Chile), LRI.
    Starting: March 2013. Duration: 24 months.
  • Project FSF (Safe and Reliable Embedded Systems)
    Team members involved: Burkhart Wolff, Delphine Longuet, Frédéric Tuong.
    In collaboration with IRT SystemX (Palaiseau, France), CEA, Inria, Institut Mines-Télécom, Alstom Transport, APSYS, Esterel Technologies, Krono-Safe, Scaleo Chip.
    Starting: April 2013. Duration: 36 months.
  • EU IP EURO-MILS (Secure European virtualisation for trustworthy applications in critical domains)
    Team members involved: Burkhart Wolff, Yakoub Nemouchi, (Abdou Feliachi - left 2013).
    In collaboration with Technikon, SYSGO AG, Airbus France, Airbus Germany, DFKI, Jemm Research, Open Synergy, T-Systems, Thales, University of Gent, Technical University of Eindhoven.
    Starting: Oct. 2012. Duration: 36 months.
  • ANR Paral-ITP (Pervasive Parallelism in Highly-Trusted Interactive Theorem Proving Platforms)
    Team members involved: Burkhart Wolff, Delphine Longuet, Frederic Voisin, (Makarius Wenzel - left Sept. 14).
    In collaboration with INRIA Roquencourt et INRIA Saclay.
    Starting: Nov. 2011. Duration: 43 months.