Laboratoire Spécification et Vérification

Founded in 1997, the Laboratoire Spécification et Vérification (LSV) is the Computer Science laboratory of ENS de Cachan, 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.


LSV 20th Year Anniversary

Visit website for this news

In celebration of two decades of activity, LSV is hosting a workshop to look back at achievements in our field and to discuss challenges ahead. The programme include invited talks by partners and members of the laboratory.

Members, former members, and other interested colleagues are cordially invited to join us in Cachan on 11 and 12 May. Attendance is free, but registration is required.


PhD Defense: Patrick Gardy

Visit website for this news | Export event in iCalendar format

PhD Patrick Gardy

Semantics of Strategy Logic
Monday, 12 June 2017 at 2:00pm
Pavillon des Jardins, ENS Paris-Saclay

PhD Defense: Amina Doumane

Visit website for this news | Export event in iCalendar format

PhD Amina Doumane

On the infinitary proof theory of logics with fixed points
Tuesday, 27 June 2017 at 10:00am
Université Paris-Diderot, Olympe-de-Gouges building, room 255

Former LSV student breaks the SHA1 cryptographic hash function

Visit website for this news

Elie Bursztein, a former PhD student under Jean Goubault-Larrecq, and head of the anti-abuse research team at Google, Inc., Mountain View, CA, USA, has just publicized a major breach into the SHA1 cryptographic hash function, in common work between his team and Amsterdam's CWI. That attack was produced by using a combination of recent cryptoanalysis techniques run on CPU clusters and GPU clusters at Google, and allows one to produce counterfeit documents.

This attack has devastating consequences. SHA1 is used routinely to make Web sites secure, notably merchant sites (SSL/TLS), as well as email (PGP/GPG), backup systems, and is also used in everyday tools such as Git. Its estimated cost of only 110 000 USD makes it tractable.

For details of the attack, see the group's site:

LSV Statement on the Secure Electronic Documents database TES

Visit website for this news

Le Laboratoire Spécification et Vérification (LSV), laboratoire d'informatique de l'ENS Paris-Saclay et du CNRS affirme que l'instauration du nouveau fichier "titres électroniques sécurisés" prévue par le décret №2016-1460, comporte un risque inhérent majeur d'attaque, vol et détournement à l'heure où les attaquants informatiques disposent de moyens considérables et croissants. Le LSV ne connaît pas de solution technique centralisée permettant de réaliser toutes les fonctionnalités prévues par le décret tout en garantissant la confidentialité des données des citoyens.

Open Positions

See the job openings

There are several open positions for students interested in the research topics investigated at LSV, including the following funded PhD and postdoc openings:

Recent publications

Visit the corresponding web page Register to the RSS feed of LSV publications

P. Bouyer, N. Markey and V. JugéCourcelle's Theorem Made Dynamic.  Research Report 1702.05183, Computing Research Repository, February 2017. 14 pages. PDF | BibTeX )
M. González, O. Beaude, P. Bouyer, S. Lasaulce and N. MarkeyStratégies d'ordonnancement de consommation d'énergie en présence d'information imparfaite de prévisionIn GRETSI'17, September 2017. To appear. PDF | BibTeX )
S. HaddadMemoryless Determinacy of Finite Parity Games: Another Simple Proof.  Research Report hal-01541508, HAL-inria, June 2017. 7 pages. Web page | PDF | BibTeX )

About LSV

LSV Contact Information

Export in vCard format | Access information

LSV photo
LSV, CNRS & ENS de Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex, France
+33 1 47 40 75 20
+33 1 47 40 75 21

Access information


Export agenda in iCalendar format | LSV seminars page

Tue, Oct 3


EATCS Distinguished Dissertation Award 2016

Visit website for this news

EATCS Distinguished Dissertation Award 2016

Georg Zetzsche received the Distinguished Dissertation Award 2016 of the EATCS for his thesis Monoids as storage mechanisms at the University of Kaiserslautern, Germany. Georg Zetzsche is currently a post-doc at LSV in the INFINI axis.

EASST Best Paper Award at ETAPS 2016

EASST Best Paper Award at ETAPS 2016

Véronique Cortier, Antoine Dallon, and Stéphanie Delaune received the EASST Best Paper Award at ETAPS 2016 for their paper Bounding the number of agents, for equivalence too presented at POST 2016.

Stéphanie Delaune awarded ERC Starting Grant

Visit website for this news

Stéphanie Delaune  
 awarded ERC Starting Grant

Stéphanie Delaune received an ERC Starting Grant for her project POPSTAR - Physical properties Of security Protocols with an Application To contactless Systems. The objective of the project is to develop foundations and practical tools to analyse the security and privacy of modern security protocols that establish and rely on physical properties.

Stéphanie is a CNRS-Researcher, she has been a member of LSV since 2007 before joining the EMSEC team at IRISA, Rennes in September 2016.