Research at LSV

Presentation

LSV devotes most of its research efforts to the study of the specification and verification of critical systems. The aim is to develop languages and formal methods for expressing and proving correctness of those systems. This sometimes leads to the development of tools for automatizing correctness proofs or finding bugs.

The laboratory is structured around five research axes, corresponding to five applications of our techniques:

• DAHU: specification and verification of systems handling large-scale, distributed databases, such as web services.
• INFINI: automatic verification of infinite-state systems (programs involving unbounded data, communicating processes, parameterized systems, etc.)
• MEXICO: verification of distributed and concurrent systems.
• SECSI: security of information systems, from security protocols to intrusion detection.
• TEMPO: verification of real-time systems, where quantitative aspects about time are crucial for specifying and verifying correctness.

The SECSI and DAHU axes are also affiliated with INRIA Saclay - Île-de-France.

We apply our results in tight collaboration with industrial partners such as Alcatel, Électricité de France, France Télécom, STMicroelectronics, etc.

Since Nov. 2006, LSV is a member of institut Farman, which gathers five laboratories of ENS Cachan around modeling, simulation and verification of complex systems.