-
ANR SofQPro (Solutions logicielles pour l'optimisation des programmes et ressources quantiques)
L’objectif est de faire le pont entre approches théoriques de l'informatique quantique et efforts technologiques, en développant une chaîne de compilation complète et certifiée afin de programmer l’ordinateur quantique. Avec ce projet, nous visons également la diffusion de ses résultats en proposant, parmi d’autres actions, un accès en ligne aux outils et méthodes développés dans le cadre de ce projet.
Team members involved: B. Valiron (local coordinator), T. Balabonski, C. Keller.
In collaboration with the LRI team ParSys, BULL BULL SAS, CEA Saclay (Commissariat à l'Energie Atomique et aux énergies alternatives Centre de Saclay), and LORIA (Laboratoire lorrain de recherche en informatique et ses applications).
Starting: October 2017. Duration: 48 months.
-
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, C. Keller
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.
-
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.
-
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.
-
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.
-
PST (Performances des Systèmes de Transport)
Team members involved: Burkhart Wolff.
In collaboration with IRT SystemX (Palaiseau, France), Alstom, Apsys, Ansys Esterel Technologies, Kronosafe, SafeRiver, Safran.
Starting: April 2013. 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.
-
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.
-
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.
-
Team members involved: Burkhart Wolff.
In collaboration with IRT SystemX (Palaiseau, France), Alstom, Apsys, Ansys,
Esterel Technologies, Kronosafe, SafeRiver, Safran.
Starting: July 2016. Duration: 42 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. End Sept 2015.
-
ANR Paral-ITP
(Pervasive Parallelism in Highly-Trusted Interactive Theorem Proving Platforms)
Team members involved: Burkhart Wolff, Delphine Longuet, Frederic Voisin, (Makarius Wenzel .
In collaboration with INRIA Roquencourt et INRIA Saclay.
Starting: Nov. 2011. End July 2015.