Specifications and Verification Laboratory

Specification and Verification Lab (LSV)

The Specifications and Verification Laboratory (LSV) is ENS Paris-Saclay's computer science laboratory, and is also affiliated to CNRS as a joint research unit (UMR 8643).

UMR 8643

61, avenue du Président Wilson
94235 Cachan Cedex
Tel. +33 (1) 47 40 75 20


The director of LSV is Stéphane Demri, CNRS senior researcher.

The staff includes 25 permanent researchers and academics, 11 associated or visiting members, 24 PhD students, 6 administrative and technical staff and one LSV member on leave.


Research at the LSV focuses on the verification of safety-critical and embedded systems, databases and security protocols.

The LSV develops the mathematical and algorithmic foundations needed to design softwares for automated proof checking and error detection.

The LSV has six research groups:

  • DAHU: databases and verification
  • DEDUCTEAM: proof checking
  • INFINI: symbolic verification
  • MEXICO: interaction and concurrency
  • SECSI: information systems security
  • VASCO: verification and synthesis of complex systems