LoVe: Logic and Verification
Manager : Étienne André
Our team is structured in two research areas, which carry out their activities in an autonomous way :
- Types, models and programming theory.
- Modular and distributed specification and verification.
See the team report 2012-2017 for more detailed information.
| Types, models and programming theory Manager : Thomas Seiller Seminars and other events can be seen on the team’s shared calendar. The main focus of this sub-team is the use of logic-based techniques and tools for the analysis, development and formalisation of programs. We attach particular importance to the foundational study of quantitative aspects of programs, such as complexity (time, space), probabilistic behaviour and formalization of real analysis, as well as the modelling of non-determinism and concurrency. Our research also covers natural language modelling and temporal reasoning. We can group our research into two main themes : – Demonstration theory and lambda-calculus : The Curry-Howard correspondence is fundamental to our view of logic. From this perspective, our preferred model of computation is the lambda-calculus, which can be seen as the prototypical functional language. An important place is also played by linear logic, seen as a source of methodology and tools for the analysis of programs, in particular through the graphical demonstration/computation formalisms derived from it (prevue networks, sharing networks…). The Curry-Howard perspective is also at the basis of the formalization and automation of proofs developed within the team, notably in Coq. – Logic and models of computing resources : The interest in quantitative aspects in programming languages (static resource analysis, probability, quantum computation) has increased considerably in recent years. Our team tackles this type of analysis with models from linear logic, and in particular from its differential, parsimonious variant and from interaction geometry. An important theme here is implicit complexity, i.e. the study of complexity classes through logical methods. | Modular and distributed specification and verification Manager : Kaïs Klai The systems developed today are increasingly complex and their operation can have significant consequences on their environment, even irreversible: avionics, medical systems, etc. It is therefore essential to guarantee safe systems, whose operation has been verified before they are implemented. The writing of a formal specification not only allows a better understanding of the system studied, but also to formally prove, by an exhaustive verification, its correct operation, whatever the execution of the system. Our activities are based on three main research themes : – Design of formal specifications : Developing specifications is a delicate task, and it is easy to make mistakes. The formal specification framework forces greater precision, and is here underlying work that chooses an expression in UML diagrams. – Parametric, modular and distributed verification : The design of new verification techniques to combat the combinatorial explosion problem is a major focus 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 are also developing different models for malware detection and malicious behaviour discovery. |