Projects

You will find below our (non-exhaustive) list of ongoing and past projects.

 

Ongoing projects:

  • VeriAMOS (Verified Abstract Machines for Operating Systems, ANR funded project, 2019-2022): design of a framework for the implementation of verified implementations of operating systems schedulers, using domain specific languages and abstract interpretation (partnership between ANTIQUE/INRIA Paris, IRISA, LIP6/Sorbonne Université, and LIG/UGA).
  • SPARK (Static Analysis for the VErification of Spreadsheets, Proof Of Concept, ERC funded project, 2019-2020): design and implementation of a platform for the analysis, verification, and optimization of spreadsheet applications.
  • DCore (Causal debugging for concurrent systems, ANR funded project, 2019-2022): to develop a semantically well-founded, novel form of concurrent debugging, which we call causal debugging, that aims to alleviate the deficiencies of current debugging techniques for large concurrent software systems (partnership between SPADES/INRIA Rohnes-Alpes, ANTIQUE/INRIA Paris, FOCUS/INRIA Sophia,  IRIF/CNRS).
  • SAFTA (Static Analysis of Fault-Tolerant Algorithms), ANR Funded project, 2017-2020.
  • TGFßSysBio (ITMO Plan Cancer funded project, 2016-2019): microenvironment and Cancer: regulation of the activity of the TGF-beta growth factor (partnership between DYLISS/INRIA Rennes – Bretagne Atlantique and ANTIQUE/INRIA Paris).

 

Past projects:

  • AnaStaSec (Static Analysis for Security Properties, ANR funded project, 2013-2018):  formal verification of security properties of software-intensive embedded systems, using automatic static analysis techniques at different levels of representation: models, source and binary codes (partnership between ANTIQUE & PROSECCO, /INRIA Paris, Airbus Operations SAS, AMOSSYS, CEA LIST, Celtique/INRIA Rennes – Bretagne Atlantique, TrustInSoft).
  • Big Mechanism (DARPA funded project, 2014-2018): develop technology to read research abstracts and papers to extract pieces of causal mechanisms, assemble these pieces into more complete causal models, and reason over these models to produce explanations. The domain of the program is cancer biology with an emphasis on signalling pathways (partnership between Harvard Medical School, ENS Lyon/CNRS,  IRIF/CNRS. ANTIQUE/INRIA Paris).
  • MemCAD (ERC Funded project, ERC Starting Grant, PI Xavier Rival, 2011-2017): As programs manipulating complex data-structures are very difficult to verify, the goal of the MemCAD ERC project was to develop a library of memory abstract domains. These abstract domains are available as part of the MemCAD static analyzer.
  • AbstractCell (Formal Abstraction of quantitative semantics for protein-protein interaction cellular network models, ANR funded Junior Chair of Excellence, 2009-2013) : investigate formal foundations and computational aspects of both the stochastic and differential approximate semantics for rule-based models.
  • To be completed…

 

 

Comments are closed.