Ongoing projects
- BLaSST: Enhancing B Language Reasoners Using SAT and SMT Techniques, funded by ANR, 2022-2026.
- ICSPA: Interoperable and Confident Set-based Proof Assistants, funded by ANR, 2022-2026.
- ProMiS: Provable Mitigation of Side Channel through Parametric Verification (An ANR–NRF French-Singaporean project 2020-2023).
- EBRP: Enhancing Event-B and Rodin, funded by ANR, 2020-2024.
- DISCONT: Correct integration of discrete and continuous models, funded by ANR, 2018-2022.
- KaNaSA: Kanazawa-Nancy for Satistifiability and Arithmetics: Inria International Partnership with JAIST (Japan), since 2016.
Former projects
- Tools and Methodologies for Formal Specifications and for Proofs at the MSR-INRIA Joint Centre, 2007-2022.
- Matryoshka: Jasmin Blanchette’s European Research Council (ERC) Starting Grant 2016. Fast Interactive Verification through Strong Higher-Order Automation. March 2017 – February 2022.
- Formedicis: Formal methods for the development and the engineering of critical interactive systems, funded by ANR, 2017-2021.
- PARDI: Verification of parameterized distributed systems, funded by ANR, 2017-2021.
- SC², Satisfiability Checking and Symbolic Computation
Coordination and Support Activity funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689. 2016-2018. - IMPEX: Implicit and explicit semantics, funded by the ANR (Agence Nationale de la Recherche), 2013-2018.
- ADN4SE: Development of the PharOS real-time microkernel operating system, 2012-2015.
- Computer-assisted schedulability and resource access checking for concurrent Java programs using timed automata, funded by the Airbus Foundation, complemented by a grant from the Lorraine region, 2013-2015.
- AVACS: Automatic Verification and Analysis of Complex Systems, funded by DFG (Deutsche Forschungsgemeinschaft) as a Transregional Collaborative Research Center, 2004-2015.
- SMArT: Satisfiability modulo arithmetics and theories, funded by the ANR (Agence Nationale de la Recherche) and the DFG (Deutsche Forschungsgemeinschaft), complemented by a grant from the Lorraine region,
2014-2017. - MEALS: Mobility between Europe and Argentina applying Logics to Systems, funded by the 7th Framework program of the European Community under Marie Curie’s International Research Staff Exchange Scheme, 2011-2015.
- MiSMT: Modally Inspired Satisfiability Modulo Theories, funded by the STIC-AmSud program, 2013-2015.
- ADT VeriT, funded by INRIA (2012-2014).
- Amadeus Vienna-Nancy Joint Project on Proof Compression, 2012-2013.
- SMT-SAVeS: INRIA-CNPq project with Natal (Brazil)
- Decert: project on Deduction and certification, funded by the ANR (Agence Nationale de la Recherche), 2008-2012.
