Laboratoire Spécification et Vérification

Founded in 1997, the Laboratoire Spécification et Vérification (LSV) is the Computer Science laboratory of ENS Paris-Saclay, and is also affiliated to the French Centre National de la Recherche Scientifique (CNRS) as UMR 8643. Research at LSV is focused on the verification of critical software and systems, as well as on the verification of computer system security.


Safety and Privacy in the Time of Covid-19

Information technology is enrolled in the fight against the COVID-19 pandemic. Digital certificates of non-contamination, cyber-surveillance of quarantine and lockdown measures, contamination monitoring by contact tracing have already been deployed by some countries, and others are considering them.

Faced with the crisis, the temptation is great to put aside the security and privacy principles that we usually care about. One must however remain aware of potential threats: leaks, malicious exploitation by hackers or rogue states, and improper usage even by our own institutions.

We will be told that all means have been taken to secure the applications, that the data has been anonymized, will remain confidential, etc. Such claims need to be assessed in view of a few main principles that we wish to recall:

  • While it is possible to certify some aspects of program security, these theoretical guarantees do not extend to the actual deployments. Daily news is a constant reminder that masses of sensitive data can fall into the hands of malicious parties, without any possibility of reverting or alleviating the damage. In practice, one must expect security breaches and take preventive action to limit their impact.
  • Breaches of privacy are difficult to quantify, and specialists have a hard time describing precisely under what conditions a system will respect privacy. In particular, they know that the use of pseudonyms provides little protection.
  • Any system impacting the safety and privacy of citizens must be open to public scrutiny. The publication of its specification and source code are necessary prerequisites.
  • One of the best ways to limit overuses and abuses is to rely on decentralized systems as a mean of separating powers. Many techniques exist for these purposes, based on cryptography in particular. This also assumes a clear specification of which institutions will be able to use the system, and under what control. It is known that private interests can be tempted to go against the public good, but public institutions may also end up using data outside the initially planned framework.
  • The solution to these problems cannot be purely technical. Laws governing the collection and use of private data are of paramount importance, and the current crisis should not become an opportunity to soften them.

The international research community is able to put forward technical solutions that respect the above principles, and we hope that they will be mobilised to good effect in this crisis.


Professor Position in Formal Methods

Visit website for this news

The ENS Paris-Saclay opens a faculty position for a Professor in Computer Science starting September 2020. For more information and details on how to apply, please see the position announcement.

Alain Finkel at Institut Universitaire de France

Visit website for this news

Alain Finkel nominated at Institut Universitaire de France

Alain Finkel has been nominated Senior Member of the Institut Universitaire de France. He speaks about his forthcoming projects in an inverview for the INS2I of CNRS (in French).

About LSV


LSV Contact Information

Export in vCard format | Access information

LSV photo
LSV, CNRS & ENS Paris-Saclay
4 avenue des Sciences
91190 Gif-sur-Yvette, France

Access information

Quick Links


Adnane Saoud nominated for Best-Thesis Award

Visit website for this news

Adnane Saoud has been nominated for the Best-Thesis Award of GDR MACS and Club EEA with his thesis Compositional and Efficient Controller Synthesis for Cyber-Physical Systems.

ICALP 2019 Best Student Paper Award for Marie Fortin

Visit website for this news

Marie Fortin received the Best Student Paper Award in Track B at ICALP for her contribution FO = FO3 for linear orders with monotone binary relations.

CAV Award 2019

Visit website for this news

Jean-Christophe Filliâtre (CNRS, VALS / LRI), our future colleague within the Formal-Methods Lab at Paris-Saclay, receives the 2019 CAV Award, jointly with Rustan Leino, for the design and development of reusable intermediate verification languages which significantly simplified and accelerated the building of automated deductive verifiers.

The CAV award is given anually at the CAV conference for fundamental contributions to the field of Computer-Aided Verification. Two years ago, our colleagues Alain Finkel and Philippe Schnoebelen received the CAV Award 2017 for their groundbreaking work on the verification of infinite-state systems.

ETAPS 2019 Best Theory Paper Award for Jérémy Dubut

Visit website for this news

Jérémy Dubut received the Best Theory Paper Award at ETAPS 2019 for his contribution Trees in Partial Higher Dimensional Automata. After finishing his thesis at LSV in 2018, Jérémy joined the National Institute for Informatics in Tokyo.