Carbone
Team CARBONE studies limitations and hindrances in computational processes. These topics are investigated in two complementary directions: the first is the development of defense tools with the help of logic and programming theory, and the second, the analysis of the behaviour of systems, using tools from computable analysis and type theory. More precisely, the team focuses essentially on malware analysis and on fundamentals aspect of computation.
Mocqua
The goal of the MOCQUA team is to tackle challenges coming from the the emergence of new or future computational models. The models taken into consideration go beyond the classical paradigms handling finite strings of bits and consider programs working with qubits (quantum computing), programs working with functions as inputs (higher-order computation) and programs working in infinite precision (real numbers, infinite sequences, streams, coinductive data, …). The team investigates such new models and tries to solve their intrinsic problems by computational and algorithmic methods.
Mosel–VeriDis
The MOSEL-VERIDIS team contributes to methods, techniques, and tools for developing trustworthy algorithms and systems. The team works on techniques that help algorithm and system designers gain confidence that their formal models correspond to the behaviour that is intended, as well as for formally verifying that they ensure correctness properties. A high degree of automation is targeted for the investigated techniques which include model checking techniques as well as automated theorem proving for expressive languages based on first-order logic. A particular attention is also given to the integration of the developed automatic proof tools as backends for interactive proof platforms. The proposed techniques are applied to the {formal development of algorithms and systems} with applications ranging from multi- and many-core processors to large networks, cloud computing, and controllers of physical plants or embedded systems.
Pesto
The objective of the PESTO team is to build formal models and techniques, for principled, computer-aided analysis and design of security protocols and other security sensitive applications. The team contributed to many facets of the verification of protocols, including foundational results on the decidability and complexity, widening the scope of existing verification tools, their practical development and their application to case studies. The properties expected for e-voting protocols are somewhat different from the historical goals of protocols and the team works on designing flexible security definitions, automated verification of e-voting protocols and the design of such protocols. Members of the team are also interested in the design of satisfiability procedures for various verification problems expressed modulo first-order theories.
Types
The scientific project of the TYPES team is organised around two main themes, one on resource models, semantics and expressivity for modelling complex systems and expressing resource properties and another one on proof structures, proof calculi and decision in order to prove or refute such properties and also to study meta-properties like, for instance, completeness and decidability. The team aims at studying decidable fragments and new structures, issued from resource constraints, from which validity and countermodel generation can be studied. A third complementary theme on mechanised verification of meta-theoretic properties} focuses on the formalisation in Coq of some meta-properties of different logics.
