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.


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.


Hubert Comon at Institut Universitaire de France

Visit website for this news

Hubert Comon at Institut Universitaire de France

Professor Hubert Comon has been named Senior Member of the Institut Universitaire de France. During his five-year membership term, he will pursue a project on Computer Security and Formal Methods.

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

M. F. Atig, B. Bollig and P. HabermehlEmptiness of ordered multi-pushdown automata is 2ETIME-completeInternational Journal of Foundations of Computer Science, 2017. To appear. BibTeX )
S. Demri, D. Kapur and C. Weidenbach (eds.)Special Issue of Selected Extended Papers of IJCAR 2014Journal of Automated Reasoning 58(1), 2017. Web page | BibTeX )
F. ThiréReverse engineering on arithmetic proofs.  Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, August 2016. 26 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, Jun 20


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.