LoVe: Logics and Verification

Head of Team: Damiano Mazza

Our team is structured around two autonomous axes of research:

  • Types, models and theory of programming;
  • Specification, and modular and distributed verification.

It is possible to read the 2012-2017 team’s report (in french) for more detailed information.  

Types, models and theory of programming Head of Axis: Damiano Mazza The common ground for this axis research activities is the use of tools and techniques of logical nature for the analysis, the development and the formalisation of programs. Of particular importance is the foundational study of quantitative aspects of programs, such as computational complexity (time, space), probabilistic behaviours and the formalisation of real analysis, as well as modelling non-determinism and concurrency. Our research also covers natural language modelling and temporal reasoning. Our research can be grouped into two principal themes: Proof theory and lambda-calculus: the Curry-Howard correspondence is at the core of our understanding of logic. From this perspective, our preferred model of computation is the lambda-calculus, which can be understood as the prototypical functional programming language. An important role is also played by linear logic, envisioned as a source of methods and tools for program analyses, in particular through specific formalisations of proofs and/or graphical calculus stemming from it (proof nets, sharing graphs…). The Curry-Howard point of view is also the foundational basis upon which proof formalisations and automations developed within the team, in particular based on Coq. logic and models of computational resources: Quantitative aspects of programming langages (resources static analyses, probabilities, quantum computation) have known a notable gain of interest in the recent years. Our team tackles this type of analyses using linear logic, and in particular its differential and parcimonious variants, and geometry of interaction. An important aspect is implicit complexity, namely the study of computational complexity classes through methods from logic. Specification, and modular and distributed verification Head of Axis: Kaïs Klai Systems developed nowadays are becoming more and more complex and their performance can have significant consequences on their environment, in some cases even irreversible: avionics, medical systems, etc. It is therefore essential to guarantee safe systems, whose performance have been verified before their deployment. Writing a formal specification not only allows for a better understanding of the studied system, but also to formally prove, through an exhaustive verification, its efficiency and good behaviour, regardless of the execution of the system. Our research activities are articulated around three main themes: Formal specification design: the development of specifications is a delicate task, and it is easy to make mistakes. Working with formal specifications requires better precision, thus frameworks whose specification language are UML diagrams are used. Parametric, modular and distributed verification: the design of new verification techniques to mitigate the problem of the combinatorial explosion of the state space is a main line of our research. Software safety and security: the analysis of concurrent programs is still in its infancy. We study different formalisms for modelling parallel recursive programs, and associated analysis techniques. We also develop different models for malware detection and malicious behaviour discovery.