Certified Certification Tools
Point of contact Virgile Prevosto, CEA List Summary Formal software verification tools are themselves programs, hence can contain bugs. Therefore,they should themselves be verified as much as possible, to minimize…
Towards Continuous Verification
Point of contact Virgile Prevosto, CEA List Summary Formal verification is usually understood as taking place in a traditional V development cycle, i.e., occurring at a late stage, over stable and…
Artificial Intelligence in Software Verification
Point of contact Virgile Prevosto, CEA List Summary Conversely, there are several points were AI could help the verification of programs. Notably, natural language processing techniques could be useful to…
Trusted Artificial Intelligence
Point of contact Virgile Prevosto, CEA List Summary Deep learning and neural networks have been extremely successful in many different domains. However, when it comes to trust an AI algorithm…
Quantum computation models and programming
Point of contact Pablo Arrighi, LMFMarc Baboulin, LISNSébastien Bardin, CEAVirgile Prevosto, CEA ListBenoît Valiron, LMFRenaud Vilmart, LMF Summary Even though a real quantum processor is not there yet, there are…
Security and Privacy Properties
Point of contact Virgile Prevosto, CEA List Summary Historically, formal methods have mostly focused on proving safety properties of critical embedded systems, which were relatively isolated. With the advent of…
Distributed microbiological systems
Point of contact Matthias Függer, LMF, mfuegger@lsv.frThomas Nowak, LISN, thomas.nowak@lri.fr Summary In the past few decades, synthetic biology has laid considerable focus on the re-programming of cells as computing machines. They have…
Network medicine
Point of contact Alexandre Chapoutot, ENSTA ParisFranck Delaplace, IBISC, UEVE Summary Network medicine is an emerging domain of precision medicine analysing disease through the lens of network science. Biological networks…
Formal methods for neural network-based systems
Point of contact Alexandre Chapoutot (ENSTA Paris)Franck Delaplace (IBISC, UEVE) Summary Neural networks are an important class of algorithms used in autonomous systems or robots for perception or control. The…
Data driven modeling of dynamical systems
Point of contact Alexandre Chapoutot, ENSTA ParisFranck Delaplace, IBISC, UEVE Summary Mathematical modelling of systems in order to apply formal methods may involve an important amount of knowledge on the…